:: Little {B}ezout Theorem (Factor Theorem) :: by Piotr Rudnicki :: :: Received December 30, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, CARD_3, FINSEQ_2, ARYTM_3, ORDINAL4, TARSKI, NAT_1, XXREAL_0, REAL_1, ARYTM_1, XBOOLE_0, ORDINAL1, RLVECT_1, ALGSTR_0, SUPINF_2, PARTFUN1, FINSET_1, FUNCT_2, MCART_1, ZFMISC_1, PRE_POLY, FUNCT_4, FUNCOP_1, VALUED_0, PBOOLE, XREAL_0, SGRAPH1, FINSOP_1, BINOP_1, GROUP_1, STRUCT_0, POLYNOM1, POLYNOM3, AFINSQ_1, MESFUNC1, ALGSEQ_1, VECTSP_1, POLYNOM5, LATTICES, VECTSP_2, COMPLFLD, POLYNOM2, FVSUM_1, MEMBERED, CLASSES1, UPROOTS; notations TARSKI, XBOOLE_0, XTUPLE_0, XCMPLX_0, XXREAL_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XREAL_0, ZFMISC_1, REAL_1, VECTSP_2, BINOP_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_2, DOMAIN_1, FUNCT_2, XXREAL_2, VALUED_0, NAT_1, NAT_D, STRUCT_0, ALGSTR_0, RLVECT_1, VFUNCT_1, VECTSP_1, FINSOP_1, NORMSP_1, GROUP_4, RVSUM_1, ALGSEQ_1, COMPLFLD, POLYNOM3, POLYNOM4, POLYNOM5, FINSET_1, MCART_1, FUNCT_4, FUNCOP_1, CLASSES1, FVSUM_1, WSIERP_1, MEMBERED, GROUP_1, RECDEF_1, PRE_POLY; constructors WELLORD2, SETWISEO, REAL_1, FINSEQOP, FINSOP_1, NAT_D, WSIERP_1, VECTSP_2, REALSET2, ALGSTR_1, GROUP_4, MATRIX_2, GOBOARD1, POLYNOM2, POLYNOM4, POLYNOM5, SEQ_1, RECDEF_1, BINOP_2, CLASSES1, XXREAL_2, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, PRE_POLY, POLYNOM3, POLYNOM4, POLYNOM5, FINSEQ_2, VALUED_0, XXREAL_2, FUNCT_2, RELSET_1, GROUP_1, VFUNCT_1, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions TARSKI, VECTSP_2, FUNCT_1, POLYNOM3, POLYNOM5, FINSEQ_2, RVSUM_1, GROUP_4, RLVECT_1, FUNCOP_1, RELAT_1, STRUCT_0, XTUPLE_0; theorems GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, POLYNOM5, INT_1, AXIOMS, RVSUM_1, FVSUM_1, FINSEQ_3, FINSEQ_2, POLYNOM4, POLYNOM3, FUNCT_7, ALGSEQ_1, RLVECT_1, PBOOLE, FUNCOP_1, MATRIX_3, VECTSP_2, CARD_2, FINSEQ_5, GRAPH_5, BAGORDER, RFINSEQ, WELLORD2, CARD_3, ORDINAL1, FINSOP_1, MONOID_0, INTEGRA1, FUNCT_4, MCART_1, XREAL_1, GROUP_4, XXREAL_0, PARTFUN1, XXREAL_2, NAT_D, FINSEQ_4, CLASSES1, PRE_POLY, TREES_9; schemes NAT_1, FUNCT_1, FUNCT_2, FRAENKEL, ALGSEQ_1, FINSEQ_1, RECDEF_1, CLASSES1, INT_1; begin :: Preliminaries theorem Th1: for f being FinSequence of NAT st for i being Element of NAT st i in dom f holds f.i <> 0 holds Sum f = len f iff f = (len f) |-> 1 proof defpred P[Element of NAT] means for f being FinSequence of NAT st len f = $1 & for i being Element of NAT st i in dom f holds f.i <> 0 holds Sum f = len f iff f = (len f) |-> 1; let f be FinSequence of NAT; A1: for n being Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume A2: P[n]; let f be FinSequence of NAT such that A3: len f = n+1 and A4: for i being Element of NAT st i in dom f holds f.i <> 0; consider g being FinSequence of NAT, a being Element of NAT such that A5: f = g^<*a*> by A3,FINSEQ_2:19; A6: now let i be Element of NAT; A7: dom g c= dom f by A5,FINSEQ_1:26; assume A8: i in dom g; then f.i = g.i by A5,FINSEQ_1:def 7; hence g.i <> 0 by A4,A8,A7; end; n+1 = len g + len <*a*> by A3,A5,FINSEQ_1:22; then A9: n+1 = len g + 1 by FINSEQ_1:40; then dom f = Seg len f & f.len f = a by A3,A5,FINSEQ_1:42,def 3; then a <> 0 by A3,A4,FINSEQ_1:4; then A10: 0 qua Nat+1 <= a by NAT_1:13; A11: g is FinSequence of REAL by FINSEQ_2:24; hereby reconsider h = (len g) |-> (1 qua Real) as FinSequence of REAL; reconsider h1=h as Element of (len h)-tuples_on REAL by FINSEQ_2:92; reconsider g1=g as Element of (len g)-tuples_on REAL by A11,FINSEQ_2:92; assume A12: Sum f = len f; A13: Sum g = Sum g +a -a .= n+1 -a by A3,A5,A12,RVSUM_1:74; A14: now let j be Nat; reconsider a = j as Element of NAT by ORDINAL1:def 12; assume A15: j in Seg len g; then j in dom g by FINSEQ_1:def 3; then g.j <> 0 by A6; then 0 qua Nat+1 <= g.a by NAT_1:13; hence h1.j <= g1.j by A15,FUNCOP_1:7; end; A16: Sum h1 <= Sum g1 by A14,RVSUM_1:82; Sum h = n*1 by A9,RVSUM_1:80 .= n; then n+a <= n+1-a+a by A16,A13,XREAL_1:6; then a <= 1 by XREAL_1:6; then A17: a = 1 by A10,XXREAL_0:1; then g = (len g) |-> 1 by A2,A9,A6,A13; hence f = (len f) |-> 1 by A3,A5,A9,A17,FINSEQ_2:60; end; assume f = (len f) |-> 1; then A18: f = (n |-> 1)^(1 |-> 1) by A3,FINSEQ_2:123 .= (n |-> 1)^<*1*> by FINSEQ_2:59; then A19: a = 1 by A5,FINSEQ_2:17; A20: Sum f = Sum g + a by A5,RVSUM_1:74; g = (len g) |-> 1 by A5,A9,A18,FINSEQ_2:17; hence thesis by A2,A3,A9,A6,A20,A19; end; A21: P[ 0 ] proof let f be FinSequence of NAT such that A22: len f = 0 and for i being Element of NAT st i in dom f holds f.i <> 0; hereby assume Sum f = len f; thus f = {} by A22 .= (len f) |-> 1 by A22; end; assume f = (len f) |-> 1; f = {} by A22; hence thesis by RVSUM_1:72; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A21, A1); hence thesis; end; :: Stolen from POLYNOM2 scheme IndFinSeq0 { k() -> Nat, P[set]} : for i being Element of NAT st 1 <= i & i <= k() holds P[i] provided A1: P[1] and A2: for i being Element of NAT st 1 <= i & i < k() holds P[i] implies P[ i+1] proof defpred Q[Nat] means 1 <= $1 & $1 <= k() & not P[$1]; assume not for i being Element of NAT st 1 <= i & i <= k() holds P[i]; then A3: ex k being Nat st Q[k]; consider k being Nat such that A4: Q[k] & for k9 being Nat st Q[k9] holds k <= k9 from NAT_1:sch 5(A3); per cases; suppose k = 1; hence thesis by A1,A4; end; suppose A5: k <> 1; 1 - 1 <= k - 1 by A4,XREAL_1:9; then reconsider k9 = k - 1 as Element of NAT by INT_1:3; A6: (k - 1) + 1 = k + (0 qua Nat); 1 < k by A4,A5,XXREAL_0:1; then A7: 1 <= k9 by A6,NAT_1:13; k9 <= k9 + 1 & k9 <> k9 + 1 by NAT_1:11; then A8: k9 < k by XXREAL_0:1; then k9 < k() by A4,XXREAL_0:2; hence thesis by A2,A4,A6,A8,A7; end; end; theorem Th2: for L be add-associative right_zeroed right_complementable non empty addLoopStr, r be FinSequence of L st len r >= 2 & for k being Element of NAT st 2 < k & k in dom r holds r.k = 0.L holds Sum r = r/.1 + r/.2 proof let L be add-associative right_zeroed right_complementable non empty addLoopStr, r being FinSequence of L such that A1: len r >= 2 and A2: for k being Element of NAT st 2 < k & k in dom r holds r.k = 0.L; A3: 2 in dom r by A1,FINSEQ_3:25; 1 <= len r by A1,XXREAL_0:2; then A4: 1 in dom r by FINSEQ_3:25; r is not empty by A1; then consider a being Element of L, r1 being FinSequence of L such that A5: a = r.1 and A6: r = <*a*>^r1 by FINSEQ_3:102; A7: len <*a*> = 1 by FINSEQ_1:40; then A8: r.2 = r1.(2-1) by A1,A6,FINSEQ_1:24 .= r1.1; A9: len r = 1 + len r1 by A6,A7,FINSEQ_1:22; now assume r1 is empty; then len r1 = 0; hence contradiction by A1,A9; end; then consider b being Element of L, r2 being FinSequence of L such that A10: b = r1.1 and A11: r1 = <*b*>^r2 by FINSEQ_3:102; A12: len <*b*> = 1 by FINSEQ_1:40; A13: now let i be Element of NAT such that A14: i in dom r2; A15: 1+i in dom r1 by A11,A12,A14,FINSEQ_1:28; 1 <= i by A14,FINSEQ_3:25; then 1 < 1+i by NAT_1:13; then A16: 1+1 < 1+(1+i) by XREAL_1:8; thus r2.i = r1.(1+i) by A11,A12,A14,FINSEQ_1:def 7 .= r.(1+(1+i)) by A6,A7,A15,FINSEQ_1:def 7 .= 0.L by A2,A6,A7,A15,A16,FINSEQ_1:28; end; thus Sum r = a + Sum r1 by A6,FVSUM_1:72 .= a + (b + Sum r2) by A11,FVSUM_1:72 .= a + (b + 0.L) by A13,POLYNOM3:1 .= a+b by RLVECT_1:def 4 .= r/.1 + b by A5,A4,PARTFUN1:def 6 .= r/.1 + r/.2 by A10,A3,A8,PARTFUN1:def 6; end; begin :: Canonical ordering of a finite set into a finite sequence registration let A be finite set; cluster one-to-one onto for FinSequence of A; existence proof defpred P[Element of NAT,set,set] means $3 = [choose $2`2, $2`2 \ {choose $2`2}]; set cA = card A; A1: for n being Element of NAT st 1 <= n & n < cA for x being set ex y being set st P[n,x,y]; consider f being FinSequence such that A2: len f = cA and A3: f.1 = [choose A, A \ {choose A}] or cA = 0 and A4: for n being Element of NAT st 1<=n&n {} by A2,A7,A16,CARD_1:27; then choose (f.i)`2 in (f.i)`2 by A15; hence f.(i+1) in [: A, bool A :] by A10,A9,A12,A13,ZFMISC_1:def 2; reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set by A15; take XX; thus XX = (f.(i+1))`2 by A9,MCART_1:7; {choose (f.i)`2} c= (f.i)`2 by A15,A17,ZFMISC_1:31; then (f.i)`2 = {choose (f.i)`2} \/ ((f.i)`2 \ {choose (f.i)`2}) by XBOOLE_1:45; then card X = card XX + 1 by A15,A14,CARD_2:41; hence thesis by A16; end; A18: R[1] proof reconsider X = A \ {choose A} as finite set; A19: now assume choose A in A \ {choose A}; then not choose A in {choose A} by XBOOLE_0:def 5; hence contradiction by TARSKI:def 1; end; assume A20: 1 in dom f; then A <> {} by A2,FINSEQ_3:25; hence f.1 in [: A, bool A :] by A3,ZFMISC_1:def 2; take X; thus X = (f.1)`2 by A2,A3,A20,FINSEQ_3:25,MCART_1:7; 0 qua Nat+1 <= len f by A20,FINSEQ_3:25; then {choose A} c= A by A2,CARD_1:27,ZFMISC_1:31; then A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45; hence thesis by A19,CARD_2:41; end; A21: for i being Element of NAT st 1<=i & i <= len f holds R[i] from IndFinSeq0(A18, A5); rng f c= [: A, bool A :] proof let y be set; assume y in rng f; then consider i being Nat such that A22: i in dom f and A23: y = f.i by FINSEQ_2:10; 1 <= i & i <= len f by A22,FINSEQ_3:25; hence thesis by A21,A22,A23; end; then reconsider f as FinSequence of [: A, bool A :] by FINSEQ_1:def 4; deffunc F(Nat) = (f.$1)`1; consider p being FinSequence such that A24: len p = card A and A25: for k being Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch 2; A26: dom p = dom f by A2,A24,FINSEQ_3:29; rng p c= A proof let y be set; assume y in rng p; then consider i being Nat such that A27: i in dom p and A28: p.i = y by FINSEQ_2:10; p.i = (f.i)`1 & f.i in [:A, bool A:] by A25,A26,A27,FINSEQ_2:11; hence thesis by A28,MCART_1:10; end; then reconsider p as FinSequence of A by FINSEQ_1:def 4; A29: rng p = A proof set F = p; per cases; suppose A = {}; hence thesis; end; suppose A30: A <> {}; defpred P[Element of NAT] means rng (F| Seg $1) \/ (f.$1)`2 = A & ex X being finite set st X = (f.$1)`2 & card X +$1 = cA; A31: for i being Element of NAT st 1 <= i & i < len f & P[i] holds P[i +1] proof let i be Element of NAT such that A32: 1 <= i and A33: i < len f and A34: P[i]; A35: f.(i+1) = [choose (f.i)`2, (f.i)`2 \ {choose (f.i)`2}] by A2,A4,A32 ,A33; consider X being finite set such that A36: X = (f.i)`2 and A37: card X +i = cA by A34; reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set by A36; (f.i)`2 is non empty by A2,A33,A36,A37,CARD_1:27; then {choose (f.i)`2} c= (f.i)`2 by ZFMISC_1:31; then A38: (f.i)`2 = {choose (f.i)`2} \/ ((f.i)`2 \ {choose (f.i)`2}) by XBOOLE_1:45; reconsider Fi = F| Seg i, Fi1 = F| Seg (i+1) as FinSequence of A by FINSEQ_1:18; A39: i+1 <= len F by A2,A24,A33,NAT_1:13; then consider a being Element of A such that A40: Fi1 = Fi^<*a*> by A30,TREES_9:33; 1 <= i+1 by NAT_1:12; then A41: i+1 in dom F by A39,FINSEQ_3:25; A42: rng Fi1 = rng Fi \/ rng <*a*> by A40,FINSEQ_1:31 .= rng Fi \/ {a} by FINSEQ_1:39; F.(i+1) = Fi1.(i+1) & i = len Fi by A2,A24,A33,FINSEQ_1:4,17 ,FUNCT_1:49; then A43: a = F.(i+1) by A40,FINSEQ_1:42 .= (f.(i+1))`1 by A25,A41 .= choose (f.i)`2 by A35,MCART_1:7; then (f.(i+1))`2 = (f.i)`2 \ {a} by A35,MCART_1:7; hence rng (F| Seg (i+1)) \/ (f.(i+1))`2 = A by A34,A38,A42,A43, XBOOLE_1:4; take XX; thus XX = (f.(i+1))`2 by A35,MCART_1:7; now assume choose (f.i)`2 in (f.i)`2 \ {choose (f.i)`2}; then not choose (f.i)`2 in {choose (f.i)`2} by XBOOLE_0:def 5; hence contradiction by TARSKI:def 1; end; then card X = card XX + 1 by A36,A38,CARD_2:41; hence thesis by A37; end; A44: 0+1 <= len F by A24,A30,NAT_1:13; then A45: 1 in dom F by FINSEQ_3:25; A46: P[1] proof reconsider X = A \ {choose A} as finite set; reconsider F1 = (F | Seg 1) as FinSequence of A by FINSEQ_1:18; A47: now assume choose A in A \ {choose A}; then not choose A in {choose A} by XBOOLE_0:def 5; hence contradiction by TARSKI:def 1; end; 1 in Seg (0 qua Nat+1) by FINSEQ_1:4; then A48: F1.1 = F.1 by FUNCT_1:49 .= (f.1)`1 by A25,A45 .= choose A by A3,A30,MCART_1:7; ex a being Element of A st F1 = <* a *> by A30,A44,TREES_9:34; then F | Seg 1 = <* choose A *> by A48,FINSEQ_1:40; then A49: rng (F| Seg 1) = {choose A} by FINSEQ_1:39; (f.1)`2 = A \ {choose A} by A3,A30,MCART_1:7; hence rng (F| Seg 1) \/ (f.1)`2 = A by A49,XBOOLE_1:45; take X; thus X = (f.1)`2 by A3,A30,MCART_1:7; {choose A} c= A by A30,ZFMISC_1:31; then A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45; hence thesis by A47,CARD_2:41; end; A50: for i being Element of NAT st 1<=i & i<=len f holds P[i] from IndFinSeq0(A46,A31); A51: len F >= 1 by A24,A30,NAT_1:14; then consider X being finite set such that A52: X = (f.len F)`2 and A53: card X + len f = cA by A2,A24,A50; F = F | (Seg len F) by FINSEQ_3:49; then A54: rng F \/ (f.len F)`2 = A by A2,A24,A50,A51; X = {} by A2,A53; hence thesis by A54,A52; end; end; then A55: p is onto by FUNCT_2:def 3; take p; p is one-to-one by A24,A29,FINSEQ_4:62; hence thesis by A55; end; end; definition let A be finite set; func canFS(A) -> FinSequence of A equals the one-to-one onto FinSequence of A; coherence; end; registration let A be finite set; cluster canFS A -> one-to-one onto; coherence; end; theorem Th3: for A being finite set holds len canFS A = card A proof let A be finite set; rng canFS A = A by FUNCT_2:def 3; hence thesis by FINSEQ_4:62; end; registration let A be finite non empty set; cluster canFS A -> non empty; coherence proof len canFS A = card A by Th3; hence thesis; end; end; theorem Th4: for a being set holds canFS({a}) = <* a *> proof let a be set; A1: rng canFS({a}) = {a} by FUNCT_2:def 3; len canFS({a}) = card {a} by Th3 .= 1 by CARD_1:30; hence thesis by A1,FINSEQ_1:39; end; theorem Th5: for A being finite set holds (canFS A)" is Function of A, Seg card A proof let A be finite set; len canFS A = card A by Th3; then dom canFS A = Seg card A by FINSEQ_1:def 3; then A1: rng ((canFS A)") = Seg card A by FUNCT_1:33; rng canFS A = A by FUNCT_2:def 3; then dom ((canFS A)") = A by FUNCT_1:33; hence thesis by A1,FUNCT_2:1; end; begin :: More about bags definition let X be set, S be finite Subset of X, n be Element of NAT; func (S, n)-bag -> Element of Bags X equals (EmptyBag X) +* (S --> n); correctness proof set b = (EmptyBag X) +* (S --> n); A1: EmptyBag X = (X --> 0) by PRE_POLY:def 13; A2: dom (S --> n) = S by FUNCOP_1:13; A3: now let i be set; assume not i in S; hence b.i = (EmptyBag X).i by A2,FUNCT_4:11 .= 0 by PRE_POLY:52; end; A4: now let i be set such that A5: i in S; thus b.i = (S --> n).i by A2,A5,FUNCT_4:13 .= n by A5,FUNCOP_1:7; end; A6: support b is finite proof per cases; suppose A7: S is empty; now assume support b is non empty; then consider x being set such that A8: x in support b by XBOOLE_0:def 1; b.x <> 0 by A8,PRE_POLY:def 7; hence contradiction by A3,A7; end; hence thesis; end; suppose A9: S is non empty & n = 0; now assume support b is non empty; then consider x being set such that A10: x in support b by XBOOLE_0:def 1; A11: b.x <> 0 by A10,PRE_POLY:def 7; then b.x = (S-->n).x by A2,A3,FUNCT_4:13 .= 0 by A3,A9,A11,FUNCOP_1:7; hence contradiction by A10,PRE_POLY:def 7; end; hence thesis; end; suppose S is non empty & n <> 0; then for x being set holds x in S iff b.x <> 0 by A3,A4; hence thesis by PRE_POLY:def 7; end; end; dom b = dom (EmptyBag X) \/ dom (S --> n) by FUNCT_4:def 1 .= X \/ dom (S --> n) by A1,FUNCOP_1:13 .= X \/ S by FUNCOP_1:13 .= X by XBOOLE_1:12; then (EmptyBag X) +* (S --> n) is bag of X by A6,PARTFUN1:def 2 ,PRE_POLY:def 8,RELAT_1:def 18; hence thesis by PRE_POLY:def 12; end; end; theorem Th6: for X being set, S being finite Subset of X, n being Element of NAT, i being set st not i in S holds (S, n)-bag.i = 0 proof let X be set, S be finite Subset of X, n be Element of NAT, i be set such that A1: not i in S; dom (S --> n) = S by FUNCOP_1:13; hence (S, n)-bag.i = (EmptyBag X).i by A1,FUNCT_4:11 .= 0 by PRE_POLY:52; end; theorem Th7: for X being set, S being finite Subset of X, n being Element of NAT, i being set st i in S holds (S, n)-bag.i = n proof let X be set, S be finite Subset of X, n be Element of NAT, i be set such that A1: i in S; dom (S --> n) = S by FUNCOP_1:13; hence (S, n)-bag.i = (S --> n).i by A1,FUNCT_4:13 .= n by A1,FUNCOP_1:7; end; theorem Th8: for X being set, S being finite Subset of X, n being Element of NAT st n <> 0 holds support (S, n)-bag = S proof let X be set, S be finite Subset of X, n be Element of NAT; assume n <> 0; then for x being set holds x in S iff (S, n)-bag.x <> 0 by Th6,Th7; hence thesis by PRE_POLY:def 7; end; theorem for X being set, S being finite Subset of X, n being Element of NAT st S is empty or n = 0 holds (S, n)-bag = EmptyBag X proof let X be set, S be finite Subset of X, n be Element of NAT such that A1: S is empty or n = 0; now let i be set; assume i in X; per cases; suppose i in S; hence (S, n)-bag.i = 0 by A1,Th7 .= (EmptyBag X).i by PRE_POLY:52; end; suppose not i in S; hence (S, n)-bag.i = 0 by Th6 .= (EmptyBag X).i by PRE_POLY:52; end; end; hence thesis by PBOOLE:3; end; theorem Th10: for X being set, S, T being finite Subset of X, n being Element of NAT st S misses T holds (S \/ T, n)-bag = (S,n)-bag + (T,n)-bag proof let X be set, S, T be finite Subset of X, n be Element of NAT; assume S misses T; then A1: S /\ T = {} by XBOOLE_0:def 7; now let i be set such that i in X; per cases by XBOOLE_0:def 3; suppose A2: not i in S \/ T; then A3: not i in T by XBOOLE_0:def 3; A4: not i in S by A2,XBOOLE_0:def 3; thus (S \/ T, n)-bag.i = 0 by A2,Th6 .= (S,n)-bag.i + (0 qua Nat) by A4,Th6 .= (S,n)-bag.i + (T,n)-bag.i by A3,Th6 .= ((S,n)-bag + (T,n)-bag).i by PRE_POLY:def 5; end; suppose A5: i in S; then A6: not i in T by A1,XBOOLE_0:def 4; i in S \/ T by A5,XBOOLE_0:def 3; hence (S \/ T, n)-bag.i = n by Th7 .= (S,n)-bag.i + (0 qua Nat) by A5,Th7 .= (S,n)-bag.i +(T,n)-bag.i by A6,Th6 .= ((S,n)-bag + (T,n)-bag).i by PRE_POLY:def 5; end; suppose A7: i in T; then A8: not i in S by A1,XBOOLE_0:def 4; i in S \/ T by A7,XBOOLE_0:def 3; hence (S \/ T, n)-bag.i = n by Th7 .= (T,n)-bag.i + (0 qua Nat) by A7,Th7 .= (S,n)-bag.i + (T,n)-bag.i by A8,Th6 .= ((S,n)-bag + (T,n)-bag).i by PRE_POLY:def 5; end; end; hence thesis by PBOOLE:3; end; definition let X be set; mode Rbag of X is real-valued finite-support ManySortedSet of X; end; definition let A be set, b be Rbag of A; func Sum b -> real number means :Def3: ex f being FinSequence of REAL st it = Sum f & f = b*canFS(support b); existence proof set cS = canFS(support b); set f = b*cS; A1: rng f c= REAL; support b c= dom b & rng cS = support b by FUNCT_2:def 3,PRE_POLY:37; then dom f = dom cS by RELAT_1:27; then dom f = Seg len cS by FINSEQ_1:def 3; then f is FinSequence by FINSEQ_1:def 2; then reconsider f as FinSequence of REAL by A1,FINSEQ_1:def 4; take Sum f; thus thesis; end; uniqueness; end; notation let A be set, b be bag of A; synonym degree b for Sum b; end; definition let A be set, b be bag of A; redefine func degree b -> Element of NAT means :Def4: ex f being FinSequence of NAT st it = Sum f & f = b*canFS(support b); coherence proof consider f being FinSequence of REAL such that A1: degree b = Sum f and A2: f = b*canFS(support b) by Def3; rng f c= NAT proof let y be set; assume y in rng f; then consider x being set such that A3: x in dom f and A4: y = f.x by FUNCT_1:def 3; f.x = b.((canFS(support b)).x) by A2,A3,FUNCT_1:12; hence thesis by A4; end; then reconsider f as FinSequence of NAT by FINSEQ_1:def 4; Sum f is Element of NAT; hence thesis by A1; end; compatibility proof set cS = canFS(support b); let n be Element of NAT; hereby consider f being FinSequence of REAL such that A5: degree b = Sum f and A6: f = b*canFS(support b) by Def3; A7: rng f c= NAT proof let y be set; assume y in rng f; then consider x being set such that A8: x in dom f and A9: y = f.x by FUNCT_1:def 3; f.x = b.((canFS(support b)).x) by A6,A8,FUNCT_1:12; hence thesis by A9; end; assume A10: n = degree b; reconsider f as FinSequence of NAT by A7,FINSEQ_1:def 4; take f; thus n = Sum f & f = b*cS by A10,A5,A6; end; given f being FinSequence of NAT such that A11: n = Sum f & f = b*cS; rng f c= REAL; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; f = f; hence thesis by A11,Def3; end; end; theorem Th11: for A being set, b being Rbag of A st b = EmptyBag A holds Sum b = 0 proof let A be set, b be Rbag of A; set cS = canFS(support b); assume b = EmptyBag A; then support b = {} by BAGORDER:18; then b*cS = <*>NAT; hence thesis by Def3,RVSUM_1:72; end; theorem Th12: for A being set, b being bag of A st Sum b = 0 holds b = EmptyBag A proof let A be set, b be bag of A; set cS = canFS(support b); consider f being FinSequence of NAT such that A1: degree b = Sum f and A2: f = b*canFS(support b) by Def4; assume A3: degree b = 0; now assume A4: support b <> {}; A5: now consider x being set such that A6: x in support b by A4,XBOOLE_0:def 1; x in rng cS by A6,FUNCT_2:def 3; then consider i being Nat such that A7: i in dom cS and A8: cS.i = x by FINSEQ_2:10; reconsider i as Element of NAT by ORDINAL1:def 12; f.i = b.(cS.i) by A2,A7,FUNCT_1:13; then A9: f.i <> 0 by A6,A8,PRE_POLY:def 7; support b c= dom b by PRE_POLY:37; then i in dom f by A2,A6,A7,A8,FUNCT_1:11; hence ex i being Nat st i in dom f & 0 < f.i by A9; end; for i be Nat st i in dom f holds 0 <= f.i; hence contradiction by A3,A1,A5,RVSUM_1:85; end; hence thesis by BAGORDER:19; end; theorem Th13: for A being set, S being finite Subset of A, b being bag of A holds S = support b & degree b = card S iff b = (S, 1)-bag proof let A be set, S be finite Subset of A, b be bag of A; set cS = canFS(S); set f = b*cS; A1: dom b = A by PARTFUN1:def 2; set g = (card S) |-> 1; A2: len cS = card S by Th3; A3: rng cS = S by FUNCT_2:def 3; then A4: dom f = dom cS by A1,RELAT_1:27; then dom f = Seg len cS by FINSEQ_1:def 3; then reconsider f as FinSequence by FINSEQ_1:def 2; A5: len cS = len f by A4,FINSEQ_3:29; hereby set sb = (S, 1)-bag; assume that A6: S = support b and A7: degree b = card S; consider F being FinSequence of NAT such that A8: degree b = Sum F and A9: F = b*cS by A6,Def4; now let i be Element of NAT; assume i in dom F; then F.i = b.(cS.i) & cS.i in rng cS by A4,A9,FUNCT_1:3,12; hence F.i <> 0 by A6,PRE_POLY:def 7; end; then A10: F = len F |-> 1 by A2,A5,A7,A8,A9,Th1; A11: support b = support sb by A6,Th8; now thus dom b = dom sb by A1,PARTFUN1:def 2; let x be set; assume x in dom b; per cases; suppose A12: x in support b; then A13: cS".x in dom cS by A3,A6,FUNCT_1:32; then A14: cS".x in Seg len F by A4,A9,FINSEQ_1:def 3; rng cS = support b by A6,FUNCT_2:def 3; hence b.x = b.(cS.(cS".x)) by A12,FUNCT_1:35 .= F.(cS".x) by A9,A13,FUNCT_1:13 .= 1 by A10,A14,FUNCOP_1:7 .= sb.x by A6,A12,Th7; end; suppose A15: not x in support b; hence b.x = 0 by PRE_POLY:def 7 .= sb.x by A11,A15,PRE_POLY:def 7; end; end; hence b = (S, 1)-bag by FUNCT_1:2; end; rng f c= NAT proof let y be set; assume y in rng f; then consider x being set such that A16: x in dom f and A17: y = f.x by FUNCT_1:def 3; f.x = b.(cS.x) by A16,FUNCT_1:12; hence thesis by A17; end; then reconsider f as FinSequence of NAT by FINSEQ_1:def 4; assume A18: b = (S, 1)-bag; A19: rng cS = S by FUNCT_2:def 3; now thus len f = card S by A4,A2,FINSEQ_3:29; thus len g = card S by CARD_1:def 7; let i be Nat; A20: dom f = Seg card S by A4,A2,FINSEQ_1:def 3; assume A21: i in dom f; hence f.i = b.(cS.i) by FUNCT_1:12 .= 1 by A4,A19,A18,A21,Th7,FUNCT_1:3 .= g.i by A20,A21,FUNCOP_1:7; end; then A22: f = g by FINSEQ_2:9; thus S = support b by A18,Th8; then degree b = Sum f by Def4; hence degree b = (card S)*1 by A22,RVSUM_1:80 .= card S; end; theorem Th14: for A being set, S being finite Subset of A, b being Rbag of A st support b c= S ex f being FinSequence of REAL st f = b*canFS(S) & Sum b = Sum f proof let A be set, S be finite Subset of A, b be Rbag of A such that A1: support b c= S; A2: card support b <= card S by A1,NAT_1:43; set cs = canFS(support b); A3: rng cs = support b by FUNCT_2:def 3; set cS = canFS(S); set f = b*cS; len cS = card S by Th3; then A4: dom cS = Seg card S by FINSEQ_1:def 3; len cs = card support b by Th3; then A5: dom cs = Seg card support b by FINSEQ_1:def 3; consider g being FinSequence of REAL such that A6: Sum b = Sum g and A7: g = b*cs by Def3; A8: dom b = A by PARTFUN1:def 2; then A9: dom g = Seg card support b by A1,A7,A5,A3,RELAT_1:27,XBOOLE_1:1; then A10: len g = card support b by FINSEQ_1:def 3; A11: rng cS = S by FUNCT_2:def 3; then A12: dom f = Seg card S by A4,A8,RELAT_1:27; then reconsider f as FinSequence by FINSEQ_1:def 2; rng f c= rng b by RELAT_1:26; then rng f c= REAL by XBOOLE_1:1; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; take f; thus f = b*canFS(S); per cases by A2,XXREAL_0:1; suppose A13: card support b < card S; set dd = {j where j is Element of NAT : j in dom f & f.j = 0}; A14: now consider x being set such that A15: not (x in support b iff x in S) by A13,TARSKI:1; consider j being set such that A16: j in dom cS and A17: cS.j = x by A1,A11,A15,FUNCT_1:def 3; reconsider j as Element of NAT by A16; f.j =b.x by A16,A17,FUNCT_1:13; then f.j = 0 by A1,A15,PRE_POLY:def 7; then j in dd by A4,A12,A16; hence dd is non empty; end; reconsider gr = g as FinSequence of REAL; A18: dd c= dom f proof let x be set; assume x in dd; then ex j being Element of NAT st x = j & j in dom f & f.j = 0; hence thesis; end; then reconsider dd as finite non empty set by A14; consider d being Element of NAT such that A19: card S = (card support b) + d and 1 <= d by A13,FINSEQ_4:84; set h = d |-> (0 qua Real); set F = gr^h; rng canFS(dd) = dd & dd c= NAT by A18,FUNCT_2:def 3,XBOOLE_1:1; then reconsider cdd = canFS(dd) as FinSequence of NAT by FINSEQ_1:def 4; set cdi = cdd qua Function"; reconsider cdi as Function of dd, Seg card dd by Th5; reconsider cdi as Function of dd, NAT by FUNCT_2:7; deffunc Z(set) = cdi /. $1 + card support b; consider z being Function such that A20: dom z = dd and A21: for x being set st x in dd holds z.x = Z(x) from FUNCT_1:sch 3; set p = cs"*cS +* z; A22: dom cdi = dd by FUNCT_2:def 1; set cSr = cS | (dom f \ dd); now let y be set; hereby assume y in rng cSr; then consider x being set such that A23: x in dom cSr and A24: y = cSr.x by FUNCT_1:def 3; A25: cSr.x = cS.x by A23,FUNCT_1:47; x in dom cS by A23,RELAT_1:57; then reconsider j = x as Element of NAT; A26: x in findom f \ dd by A23; then not j in dd by XBOOLE_0:def 5; then A27: f.j <> 0 by A26; x in dom cS by A23,RELAT_1:57; then b.(cS.j) <> 0 by A27,FUNCT_1:13; hence y in support b by A24,A25,PRE_POLY:def 7; end; assume A28: y in support b; then consider x being set such that A29: x in dom cS and A30: y = cS.x by A1,A11,FUNCT_1:def 3; now assume x in dd; then consider j being Element of NAT such that A31: j = x and A32: j in dom f & f.j = 0; 0 = b.(cS.j) by A4,A12,A32,FUNCT_1:13; hence contradiction by A28,A30,A31,PRE_POLY:def 7; end; then x in dom f \ dd by A4,A12,A29,XBOOLE_0:def 5; hence y in rng cSr by A29,A30,FUNCT_1:50; end; then A33: rng cSr = support b by TARSKI:1; (findom f \ dd) /\ dom f = dom f \ dd by XBOOLE_1:28; then cSr is one-to-one & dom cSr = (dom f \ dd) by A4,A12,FUNCT_1:52 ,RELAT_1:61; then support b, dom f \dd are_equipotent by A33,WELLORD2:def 4; then A34: card support b = card (dom f \ dd) by CARD_1:5; card (dom f \ dd) = card dom f - card dd by A18,CARD_2:44; then A35: card support b + card dd = card S by A12,A34,FINSEQ_1:57; A36: now A37: dom (cs") = support b by A3,FUNCT_1:33; assume dom (cs"*cS) /\ dom z <> {}; then consider x being set such that A38: x in dom (cs"*cS) /\ dom z by XBOOLE_0:def 1; x in dom z by A38,XBOOLE_0:def 4; then consider j being Element of NAT such that A39: j = x and j in dom f and A40: f.j = 0 by A20; A41: x in dom (cs"*cS) by A38,XBOOLE_0:def 4; then j in dom cS by A39,FUNCT_1:11; then f.j = b.(cS.j) by FUNCT_1:13; then not cS.j in support b by A40,PRE_POLY:def 7; hence contradiction by A41,A39,A37,FUNCT_1:11; end; len F = len g + len h by FINSEQ_1:22 .= card S by A10,A19,CARD_1:def 7; then A42: dom F = Seg card S by FINSEQ_1:def 3; now let x be set; hereby assume A43: x in dom (cs"*cS) \/ dom z; per cases by A43,XBOOLE_0:def 3; suppose x in dom (cs"*cS); hence x in dom F by A4,A42,FUNCT_1:11; end; suppose x in dom z; hence x in dom F by A12,A42,A18,A20; end; end; assume A44: x in dom F; then reconsider i = x as Element of NAT; per cases; suppose f.x = 0; then i in dom z by A12,A42,A20,A44; hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 3; end; suppose A45: f.x <> 0; f.i = b.(cS.i) by A4,A42,A44,FUNCT_1:13; then cS.i in support b by A45,PRE_POLY:def 7; then cS. i in dom (cs") by A3,FUNCT_1:33; then i in dom (cs"*cS) by A4,A42,A44,FUNCT_1:11; hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 3; end; end; then A46: dom (cs"*cS) \/ dom z = dom F by TARSKI:1; then A47: dom p = dom F by FUNCT_4:def 1; len cdd = card dd by Th3; then A48: dom cdd = Seg d by A19,A35,FINSEQ_1:def 3; then A49: rng cdi = Seg d by FUNCT_1:33; A50: rng z c= Seg card S proof let y be set; assume y in rng z; then consider x being set such that A51: x in dom z and A52: y = z.x by FUNCT_1:def 3; A53: cdi/.x = cdi.x & cdi.x in Seg d by A22,A49,A20,A51,FUNCT_1:3 ,PARTFUN1:def 6; then 1 <= cdi/.x by FINSEQ_1:1; then A54: 1 <= cdi/.x + card support b by NAT_1:12; cdi/.x <= d by A53,FINSEQ_1:1; then A55: cdi/.x + card support b <= d + card support b by XREAL_1:6; y = cdi/.x + card support b by A20,A21,A51,A52; hence thesis by A19,A54,A55,FINSEQ_1:1; end; A56: now let x be set such that A57: x in dom F; per cases by A46,A57,XBOOLE_0:def 3; suppose A58: x in dom (cs"*cS); then (cs"*cS).x in rng (cs"*cS) by FUNCT_1:3; then (cs"*cS).x in rng (cs") by FUNCT_1:14; then A59: (cs"*cS).x in dom cs by FUNCT_1:33; not x in dom z by A36,A58,XBOOLE_0:def 4; then A60: p.x = (cs"*cS).x by FUNCT_4:11; Seg card support b c= Seg card S by A2,FINSEQ_1:5; hence p.x in dom F by A5,A42,A60,A59; end; suppose x in dom z; then p.x = z.x & z.x in rng z by FUNCT_1:3,FUNCT_4:13; hence p.x in dom F by A42,A50; end; end; A61: dom p = dom (cs"*cS) \/ dom z by FUNCT_4:def 1; reconsider p as Function of dom F, dom F by A47,A56,FUNCT_2:3; len h = d by CARD_1:def 7; then A62: dom h = Seg d by FINSEQ_1:def 3; A63: rng cdd = dd by FUNCT_2:def 3; now let x be set; hereby assume x in rng p; then consider a being set such that A64: a in dom p and A65: x = p.a by FUNCT_1:def 3; per cases by A64,FUNCT_4:12; suppose A66: a in dom (cs"*cS); then cS.a in dom (cs") by FUNCT_1:11; then cs".(cS.a) in rng (cs") by FUNCT_1:3; then A67: cs".(cS.a) in dom cs by FUNCT_1:33; not a in dom z by A36,A66,XBOOLE_0:def 4; then A68: p.a = (cs"*cS).a by FUNCT_4:11 .= cs".(cS.a) by A66,FUNCT_1:12; dom cs c= dom F by A5,A2,A42,FINSEQ_1:5; hence x in dom F by A65,A68,A67; end; suppose a in dom z; then z.a in rng z & p.a = z.a by FUNCT_1:3,FUNCT_4:13; hence x in dom F by A42,A50,A65; end; end; assume A69: x in dom F; then reconsider j = x as Element of NAT; per cases by A69,FINSEQ_1:25; suppose A70: j in dom gr; then A71: cs.j in support b by A5,A3,A9,FUNCT_1:3; then A72: cS".(cs.j) in Seg card S by A1,A4,A11,FUNCT_1:32; now assume cS".(cs.j) in dom z; then A73: ex k being Element of NAT st k = cS".(cs.j) & k in dom f & f.k = 0 by A20; (b*cS).(cS".(cs.j)) = b.(cS.(cS".(cs.j))) by A4,A72,FUNCT_1:13 .= b.(cs.j) by A1,A11,A71,FUNCT_1:35; hence contradiction by A71,A73,PRE_POLY:def 7; end; then p.(cS".(cs.j)) = (cs"*cS).(cS".(cs.j)) by FUNCT_4:11 .= cs".(cS.(cS".(cs.j))) by A4,A72,FUNCT_1:13 .= cs".(cs.j) by A1,A11,A71,FUNCT_1:35 .= j by A5,A9,A70,FUNCT_1:34; hence x in rng p by A42,A47,A72,FUNCT_1:3; end; suppose ex n being Nat st n in dom h & j=len gr + n; then consider n being Nat such that A74: n in dom h and A75: j = len gr + n; A76: cdd.n in dd by A62,A48,A63,A74,FUNCT_1:3; p.(cdd.n) = z.(cdd.n) by A62,A48,A63,A20,A74,FUNCT_1:3,FUNCT_4:13 .= cdi /. (cdd.n) + card support b by A62,A48,A63,A21,A74,FUNCT_1:3 .= cdi.(cdd.n) + card support b by A62,A48,A63,A22,A74,FUNCT_1:3 ,PARTFUN1:def 6 .= n + card support b by A62,A48,A74,FUNCT_1:34 .= j by A9,A75,FINSEQ_1:def 3; hence x in rng p by A12,A42,A18,A47,A76,FUNCT_1:3; end; end; then A77: rng p = dom F by TARSKI:1; then A78: dom (F*p) = dom F by A47,RELAT_1:27; now let x be set; assume A79: x in dom f; per cases; suppose A80: f.x = 0; reconsider cdix = cdi /. x as Element of NAT; reconsider px = p.x as Element of NAT; reconsider j = x as Element of NAT by A79; A81: j in dom z by A20,A79,A80; then A82: p.x = z.x by FUNCT_4:13 .= cdi /. x + card support b by A20,A21,A81; A83: cdi.x in Seg card dd by A20,A81,FUNCT_2:5; dom cdi = dd by FUNCT_2:def 1; then A84: cdi /. x = cdi.x by A20,A81,PARTFUN1:def 6; thus f.x = h.(cdix) by A80 .= F.px by A10,A19,A62,A35,A82,A84,A83,FINSEQ_1:def 7 .= (F*p).x by A12,A42,A78,A79,FUNCT_1:12; end; suppose A85: f.x <> 0; reconsider px = p.x as Element of NAT; f.x = b.(cS.x) by A79,FUNCT_1:12; then cS.x in support b by A85,PRE_POLY:def 7; then A86: cS.x in rng cs by FUNCT_2:def 3; then A87: cs".(cS.x) in dom cs by FUNCT_1:32; now assume x in dd; then ex j being Element of NAT st j=x & j in dom f & f.j = 0; hence contradiction by A85; end; then A88: p.x = (cs"*cS).x by A20,FUNCT_4:11 .= cs".(cS.x) by A4,A12,A79,FUNCT_1:13; thus f.x = b.(cS.x) by A79,FUNCT_1:12 .= b.(cs.px) by A86,A88,FUNCT_1:32 .= g.(px) by A7,A87,A88,FUNCT_1:13 .= F.(px) by A5,A9,A87,A88,FINSEQ_1:def 7 .= (F*p).x by A12,A42,A78,A79,FUNCT_1:12; end; end; then A89: f = F*p by A4,A11,A8,A42,A78,FUNCT_1:2,RELAT_1:27; A90: p is one-to-one proof let a, c be set such that A91: a in dom p & c in dom p and A92: p.a = p.c; per cases by A61,A91,XBOOLE_0:def 3; suppose A93: a in dom (cs"*cS) & c in dom (cs"*cS); then cS.a in dom (cs") by FUNCT_1:11; then cS.a in rng cs by FUNCT_1:33; then A94: cs.(cs".(cS.a)) = cS.a by FUNCT_1:35; a in dom cS by A93,FUNCT_1:11; then A95: cS".(cS.a) = a by FUNCT_1:34; cS.c in dom (cs") by A93,FUNCT_1:11; then A96: cS.c in rng cs by FUNCT_1:33; not c in dom z by A36,A93,XBOOLE_0:def 4; then A97: p.c = (cs"*cS).c by FUNCT_4:11 .= cs".(cS.c) by A93,FUNCT_1:12; A98: c in dom cS by A93,FUNCT_1:11; not a in dom z by A36,A93,XBOOLE_0:def 4; then p.a = (cs"*cS).a by FUNCT_4:11 .= cs".(cS.a) by A93,FUNCT_1:12; then cS".(cS.a) = cS".(cS.c) by A92,A97,A94,A96,FUNCT_1:35; hence thesis by A95,A98,FUNCT_1:34; end; suppose A99: a in dom (cs"*cS) & c in dom z; then cS.a in dom (cs") by FUNCT_1:11; then cs".(cS.a) in rng (cs") by FUNCT_1:3; then A100: cs".(cS.a) in dom cs by FUNCT_1:33; not a in dom z by A36,A99,XBOOLE_0:def 4; then A101: p.a = (cs"*cS).a by FUNCT_4:11 .= cs".(cS.a) by A99,FUNCT_1:12; p.c = z.c by A99,FUNCT_4:13 .= cdi /. c + card support b by A20,A21,A99; then cdi /. c + card support b <= (0 qua Nat)+card support b by A5,A92 ,A101,A100,FINSEQ_1:1; then cdi /. c = 0 by XREAL_1:6; then A102: cdi.c = 0 by A22,A20,A99,PARTFUN1:def 6; cdi.c in rng cdi by A22,A20,A99,FUNCT_1:3; hence thesis by A49,A102,FINSEQ_1:1; end; suppose A103: a in dom z & c in dom (cs"*cS); then cS.c in dom (cs") by FUNCT_1:11; then cs".(cS.c) in rng (cs") by FUNCT_1:3; then A104: cs".(cS.c) in dom cs by FUNCT_1:33; not c in dom z by A36,A103,XBOOLE_0:def 4; then A105: p.c = (cs"*cS).c by FUNCT_4:11 .= cs".(cS.c) by A103,FUNCT_1:12; p.a = z.a by A103,FUNCT_4:13 .= cdi /. a + card support b by A20,A21,A103; then cdi /. a + card support b <= (0 qua Nat)+card support b by A5,A92 ,A105,A104,FINSEQ_1:1; then cdi /. a = 0 by XREAL_1:6; then A106: cdi.a = 0 by A22,A20,A103,PARTFUN1:def 6; cdi.a in rng cdi by A22,A20,A103,FUNCT_1:3; hence thesis by A49,A106,FINSEQ_1:1; end; suppose A107: a in dom z & c in dom z; then A108: cdi /. a = cdi . a & cdi /. c = cdi . c by A22,A20,PARTFUN1:def 6; A109: p.c = z.c by A107,FUNCT_4:13 .= cdi /. c + card support b by A20,A21,A107; p.a = z.a by A107,FUNCT_4:13 .= cdi /. a + card support b by A20,A21,A107; hence thesis by A22,A20,A92,A107,A109,A108,FUNCT_1:def 4; end; end; Sum h = 0 by RVSUM_1:81; then A110: Sum gr = Sum gr + Sum h .= Sum F by RVSUM_1:75; p is onto by A77,FUNCT_2:def 3; hence thesis by A6,A90,A89,A110,FINSOP_1:7; end; suppose card support b = card S; hence thesis by A1,A6,A7,PRE_POLY:8; end; end; theorem Th15: for A being set, b, b1, b2 being Rbag of A st b = b1 + b2 holds Sum b = Sum b1 + Sum b2 proof let A be set, b, b1, b2 be Rbag of A; set S = support b; set SS = support b1 \/ support b2; A1: dom b2 = A by PARTFUN1:def 2; then A2: support b2 c= A by PRE_POLY:37; A3: dom b1 = A by PARTFUN1:def 2; then support b1 c= A by PRE_POLY:37; then reconsider SS as finite Subset of A by A2,XBOOLE_1:8; set cS = canFS SS; consider f1r being FinSequence of REAL such that A4: f1r = b1*canFS(SS) and A5: Sum b1 = Sum f1r by Th14,XBOOLE_1:7; A6: rng cS = SS by FUNCT_2:def 3; then A7: dom f1r = dom cS by A3,A4,RELAT_1:27; assume A8: b = b1 + b2; then S c= SS by PRE_POLY:75; then consider f being FinSequence of REAL such that A9: f = b*canFS(SS) and A10: Sum b = Sum f by Th14; dom b = A by PARTFUN1:def 2; then A11: dom f = dom cS by A9,A6,RELAT_1:27; then A12: len f1r = len f by A7,FINSEQ_3:29; consider f2r being FinSequence of REAL such that A13: f2r = b2*canFS(SS) and A14: Sum b2 = Sum f2r by Th14,XBOOLE_1:7; A15: dom f2r = dom cS by A1,A13,A6,RELAT_1:27; A16: now let k be Element of NAT such that A17: k in dom f1r; A18: f1r/.k = f1r.k by A17,PARTFUN1:def 6 .= b1.(cS.k) by A4,A17,FUNCT_1:12; A19: f.k = b.(cS.k) by A9,A11,A7,A17,FUNCT_1:12; f2r/.k = f2r.k by A7,A15,A17,PARTFUN1:def 6 .= b2.(cS.k) by A13,A7,A15,A17,FUNCT_1:12; hence f.k = f1r/.k + f2r/.k by A8,A18,A19,PRE_POLY:def 5; end; len f1r = len f2r by A7,A15,FINSEQ_3:29; hence thesis by A10,A5,A14,A12,A16,INTEGRA1:21; end; theorem Th16: :: GROUP_4:18 but about a different Product for L being associative commutative unital non empty multMagma , f, g being FinSequence of L, p being Permutation of dom f st g = f * p holds Product(g) = Product(f) proof let L be associative commutative unital non empty multMagma, f, g be FinSequence of L, p be Permutation of dom f such that A1: g = f * p; set mL = (the multF of L); mL is commutative & mL is associative by MONOID_0:def 11; hence thesis by A1,FINSOP_1:7; end; begin :: More on polynomials definition let L be non empty ZeroStr, p be Polynomial of L; attr p is non-zero means :Def5: p <> 0_. L; end; theorem Th17: for L being non empty ZeroStr, p being Polynomial of L holds p is non-zero iff len p > 0 proof let L be non empty ZeroStr, p be Polynomial of L; hereby assume p is non-zero; then p <> 0_. L by Def5; then len p <> 0 by POLYNOM4:5; hence len p > 0; end; assume len p > 0; then p <> 0_. L by POLYNOM4:3; hence thesis by Def5; end; registration let L be non trivial ZeroStr; cluster non-zero for Polynomial of L; existence proof set a = the Element of NonZero L; reconsider a as Element of L; take p = <%a%>; A1: ( not a in {0.L})& (0_. L).0 = 0.L by FUNCOP_1:7,XBOOLE_0:def 5; p.0 = a by POLYNOM5:32; then p <> 0_. L by A1,TARSKI:def 1; hence thesis by Def5; end; end; registration let L be non degenerated non empty multLoopStr_0, x be Element of L; cluster <%x, 1.L%> -> non-zero; correctness proof len <%x, 1.L%> = 2 by POLYNOM5:40; hence thesis by Th17; end; end; theorem Th18: for L being non empty ZeroStr, p being Polynomial of L st len p > 0 holds p.(len p -'1) <> 0.L proof let L be non empty ZeroStr, p be Polynomial of L; assume len p > 0; then ex k being Nat st len p = k+1 by NAT_1:6; then len p = (len p -'1)+1 by NAT_D:34; hence thesis by ALGSEQ_1:10; end; theorem Th19: for L being non empty ZeroStr, p being AlgSequence of L st len p = 1 holds p = <%p.0%> & p.0 <> 0.L proof let L be non empty ZeroStr, p being AlgSequence of L such that A1: len p = 1; thus p=<%p.0%> by A1,ALGSEQ_1:def 5; hence thesis by A1,ALGSEQ_1:14; end; theorem Th20: :: from POLYNOM4:5 right-distributive for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, p be Polynomial of L holds p*'( 0_.(L)) = 0_.(L) proof let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, p be Polynomial of L; now let i be Element of NAT; consider r be FinSequence of L such that len r = i+1 and A1: (p*'(0_.(L))).i = Sum r and A2: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * (0_. L).(i+1-'k) by POLYNOM3:def 9; now let k be Element of NAT; assume k in dom r; hence r.k = p.(k-'1) * (0_. L).(i+1-'k) by A2 .= p.(k-'1) * 0.L by FUNCOP_1:7 .= 0.L by VECTSP_1:6; end; hence (p*'(0_.(L))).i = 0.L by A1,POLYNOM3:1 .= (0_.(L)).i by FUNCOP_1:7; end; hence thesis by FUNCT_2:63; end; registration cluster algebraic-closed add-associative right_zeroed right_complementable Abelian commutative associative distributive domRing-like non degenerated for unital non empty doubleLoopStr; existence proof take F_Complex; thus thesis; end; end; theorem Th21: for L being add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p, q being Polynomial of L st p*'q = 0_. L holds p = 0_. L or q = 0_. L proof let L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p, q being Polynomial of L such that A1: p*'q = 0_. L and A2: p <> 0_. L and A3: q <> 0_. L; consider lp1 being Nat such that A4: len p = lp1+1 by A2,NAT_1:6,POLYNOM4:5; len p <> 0 by A2,POLYNOM4:5; then A5: 0 qua Nat+1 <= len p by NAT_1:13; consider lq1 being Nat such that A6: len q = lq1+1 by A3,NAT_1:6,POLYNOM4:5; reconsider lp1, lq1 as Element of NAT by ORDINAL1:def 12; A7: p.lp1 <> 0.L by A4,ALGSEQ_1:10; A8: q.lq1 <> 0.L by A6,ALGSEQ_1:10; set lpq = lp1 + lq1; consider r being FinSequence of L such that A9: len r = lpq+1 and A10: (p*'q).lpq = Sum r and A11: for k be Element of NAT st k in dom r holds r.k=p.(k-'1)*q.(lpq+1-' k) by POLYNOM3:def 9; A12: lpq+1-'len p = lq1+(lp1+1)-'len p .= lq1 by A4,NAT_D:34; len p <= lp1+1+lq1 by A4,NAT_1:12; then A13: len p in dom r by A9,A5,FINSEQ_3:25; now let k be Nat such that A14: k in dom r and A15: k <> len p; reconsider k1=k as Element of NAT by ORDINAL1:def 12; A16: r.k1 = p.(k1-'1) * q.(lpq+1-'k1) by A11,A14; per cases by A15,XXREAL_0:1; suppose k < len p; then consider d being Element of NAT such that A17: len p = k1+d and A18: 1 <= d by FINSEQ_4:84; A19: len q <= lq1+d by A6,A18,XREAL_1:6; lpq+1-'k = lq1+d+k-'k by A4,A17 .= lq1+d by NAT_D:34; hence r.k = p.(k-'1)*0.L by A16,A19,ALGSEQ_1:8 .= 0.L by VECTSP_1:6; end; suppose k > len p; then k >= len p + 1 by NAT_1:13; then k-'1 >= len p + 1-'1 by NAT_D:42; then k-'1 >= len p by NAT_D:34; hence r.k = 0.L * q.(lpq+1-'k) by A16,ALGSEQ_1:8 .= 0.L by VECTSP_1:7; end; end; then Sum r = r.(len p) by A13,MATRIX_3:12 .= p.(len p -'1)*q.(lpq+1-'len p) by A11,A13 .= p.lp1 * q.lq1 by A4,A12,NAT_D:34; then Sum r <> 0.L by A7,A8,VECTSP_2:def 1; hence contradiction by A1,A10,FUNCOP_1:7; end; registration let L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr; cluster Polynom-Ring L -> domRing-like; correctness proof set PRL = Polynom-Ring L; let x, y be Element of PRL; reconsider xp = x, yp = y as Polynomial of L by POLYNOM3:def 10; A1: 0_. L = 0.PRL by POLYNOM3:def 10; assume x*y = 0.PRL; then xp*'yp = 0_. L by A1,POLYNOM3:def 10; hence thesis by A1,Th21; end; end; registration let L be domRing, p, q be non-zero Polynomial of L; cluster p*'q -> non-zero; correctness proof p <> 0_. L & q <> 0_. L by Def5; then p*'q <> 0_. L by Th21; hence thesis by Def5; end; end; theorem for L being non degenerated comRing, p, q being Polynomial of L holds Roots p \/ Roots q c= Roots (p*'q) proof let L be non degenerated comRing, p, q being Polynomial of L; let x be set; assume A1: x in Roots p \/ Roots q; per cases by A1,XBOOLE_0:def 3; suppose A2: x in Roots p; then reconsider a = x as Element of L; a is_a_root_of p by A2,POLYNOM5:def 9; then eval(p,a) = 0.L by POLYNOM5:def 6; then eval(p,a) * eval(q,a) = 0.L by VECTSP_1:7; then eval(p*'q,a) = 0.L by POLYNOM4:24; then a is_a_root_of p*'q by POLYNOM5:def 6; hence thesis by POLYNOM5:def 9; end; suppose A3: x in Roots q; then reconsider a = x as Element of L; a is_a_root_of q by A3,POLYNOM5:def 9; then eval(q,a) = 0.L by POLYNOM5:def 6; then eval(p,a) * eval(q,a) = 0.L by VECTSP_1:6; then eval(p*'q,a) = 0.L by POLYNOM4:24; then a is_a_root_of p*'q by POLYNOM5:def 6; hence thesis by POLYNOM5:def 9; end; end; theorem Th23: for L being domRing, p, q being Polynomial of L holds Roots (p*' q) = Roots p \/ Roots q proof let L be domRing, p, q being Polynomial of L; now let x be set; hereby assume A1: x in Roots (p*'q); then reconsider a = x as Element of L; a is_a_root_of p*'q by A1,POLYNOM5:def 9; then eval(p*'q,a) = 0.L by POLYNOM5:def 6; then A2: eval(p,a) * eval(q,a) = 0.L by POLYNOM4:24; per cases by A2,VECTSP_2:def 1; suppose eval(p,a) = 0.L; then a is_a_root_of p by POLYNOM5:def 6; then a in Roots p by POLYNOM5:def 9; hence x in Roots p \/ Roots q by XBOOLE_0:def 3; end; suppose eval(q,a) = 0.L; then a is_a_root_of q by POLYNOM5:def 6; then a in Roots q by POLYNOM5:def 9; hence x in Roots p \/ Roots q by XBOOLE_0:def 3; end; end; assume A3: x in Roots p \/ Roots q; per cases by A3,XBOOLE_0:def 3; suppose A4: x in Roots p; then reconsider a = x as Element of L; a is_a_root_of p by A4,POLYNOM5:def 9; then eval(p,a) = 0.L by POLYNOM5:def 6; then eval(p,a) * eval(q,a) = 0.L by VECTSP_1:7; then eval(p*'q,a) = 0.L by POLYNOM4:24; then a is_a_root_of p*'q by POLYNOM5:def 6; hence x in Roots (p*'q) by POLYNOM5:def 9; end; suppose A5: x in Roots q; then reconsider a = x as Element of L; a is_a_root_of q by A5,POLYNOM5:def 9; then eval(q,a) = 0.L by POLYNOM5:def 6; then eval(p,a) * eval(q,a) = 0.L by VECTSP_1:6; then eval(p*'q,a) = 0.L by POLYNOM4:24; then a is_a_root_of p*'q by POLYNOM5:def 6; hence x in Roots (p*'q) by POLYNOM5:def 9; end; end; hence thesis by TARSKI:1; end; theorem Th24: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p being (Polynomial of L), pc being ( Element of Polynom-Ring L) st p = pc holds -p = -pc proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be (Polynomial of L), pc be (Element of Polynom-Ring L) such that A1: p = pc; set PRL = Polynom-Ring L; reconsider mpc = -p as Element of PRL by POLYNOM3:def 10; p+-p = p-p .= 0_. L by POLYNOM3:29; then pc + mpc = 0_. L by A1,POLYNOM3:def 10 .= 0.PRL by POLYNOM3:def 10; hence thesis by RLVECT_1:def 10; end; theorem Th25: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being (Polynomial of L), pc, qc being (Element of Polynom-Ring L) st p= pc & q = qc holds p-q = pc-qc proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be (Polynomial of L), pc,qc be (Element of Polynom-Ring L) such that A1: p = pc and A2: q = qc; -q = -qc by A2,Th24; hence thesis by A1,POLYNOM3:def 10; end; theorem Th26: for L being Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q, r being ( Polynomial of L) holds p*'q-p*'r = p*'(q-r) proof let L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q, r be (Polynomial of L); set PRL = Polynom-Ring L; reconsider pc = p, qc = q, rc = r as Element of PRL by POLYNOM3:def 10; A1: qc-rc = q-r by Th25; p*'q = pc*qc & p*'r = pc*rc by POLYNOM3:def 10; hence p*'q-p*'r = pc*qc - pc*rc by Th25 .= pc*(qc-rc) by VECTSP_1:11 .= p*'(q-r) by A1,POLYNOM3:def 10; end; theorem Th27: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being (Polynomial of L) st p-q = 0_. L holds p = q proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, q, r be (Polynomial of L); set PRL = Polynom-Ring L; reconsider qc = q, rc = r as Element of PRL by POLYNOM3:def 10; assume A1: q-r = 0_. L; 0_. L = 0.PRL by POLYNOM3:def 10; then qc-rc = 0.PRL by A1,Th25; hence thesis by VECTSP_1:27; end; theorem Th28: for L being Abelian add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p, q, r being Polynomial of L st p <> 0_. L & p*'q = p*'r holds q = r proof let L be Abelian add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p, q, r be Polynomial of L ; assume A1: p <> 0_. L; assume p*'q = p*'r; then p*'q-p*'r = 0_. L by POLYNOM3:29; then p*'(q-r) = 0_. L by Th26; then q-r = 0_. L by A1,Th21; hence thesis by Th27; end; theorem Th29: for L being domRing, n being Element of NAT, p being Polynomial of L st p <> 0_. L holds p`^n <> 0_. L proof let L be domRing, n be Element of NAT, p be Polynomial of L; defpred P[Element of NAT] means p`^$1 <> 0_. L; assume A1: p <> 0_. L; A2: for n being Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT such that A3: P[n]; p`^(n+1) = (p`^n) *' p by POLYNOM5:19; hence thesis by A1,A3,Th21; end; (1_. L).0 = 1.L & (0_. L).0 = 0.L by FUNCOP_1:7,POLYNOM3:30; then A4: P[ 0 ] by POLYNOM5:15; for n being Element of NAT holds P[n] from NAT_1:sch 1(A4,A2); hence thesis; end; theorem Th30: for L being comRing, i, j being Element of NAT, p being Polynomial of L holds (p`^i) *' (p`^j) = p `^(i+j) proof let L be comRing, i, j being Element of NAT, p be Polynomial of L; defpred P[Element of NAT] means (p`^i) *' (p`^$1) = p `^(i+$1); A1: for j being Element of NAT st P[j] holds P[j+1] proof let j be Element of NAT such that A2: P[j]; (p`^i) *' (p`^(j+1)) = (p`^i) *' ((p`^j) *' p) by POLYNOM5:19 .= (p`^(i+j)) *' p by A2,POLYNOM3:33 .= p`^(i+j+1) by POLYNOM5:19 .= p`^(i+(j+1)); hence thesis; end; (p`^i) *' (p`^0) = (p`^i) *' 1_. L by POLYNOM5:15 .= (p`^(i+(0 qua Nat))) by POLYNOM3:35; then A3: P[ 0 ]; for j being Element of NAT holds P[j] from NAT_1:sch 1(A3,A1); hence thesis; end; theorem Th31: for L being non empty multLoopStr_0 holds 1_.(L) = <%1.L%> proof let L be non empty multLoopStr_0; A1: dom 0_.(L) = NAT by FUNCT_2:def 1; now let x be set; assume x in NAT; then reconsider n = x as Element of NAT; per cases; suppose A2: x = 0; hence (1_.(L)).x = 1.L by A1,FUNCT_7:31 .= <%1.L%>.x by A2,ALGSEQ_1:def 5; end; suppose A3: n <> 0; then A4: n = 1 or n > 1 by NAT_1:53; thus (1_.(L)).x = (0_.(L)).n by A3,FUNCT_7:32 .= 0.L by FUNCOP_1:7 .= <%1.L%>.x by A4,POLYNOM5:32; end; end; hence thesis by FUNCT_2:12; end; theorem for L being add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, p being Polynomial of L holds p*'<%1.L%> = p proof let L be add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, p being Polynomial of L; thus p*'<%1.L%> = p*'1_.(L) by Th31 .= p by POLYNOM3:35; end; theorem Th33: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being Polynomial of L st len p = 0 or len q = 0 holds len (p*'q) = 0 proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being Polynomial of L; assume A1: len p = 0 or len q = 0; per cases by A1; suppose len p = 0; then p = 0_. L by POLYNOM4:5; then p*'q = 0_. L by POLYNOM4:2; hence thesis by POLYNOM4:3; end; suppose len q = 0; then q = 0_. L by POLYNOM4:5; then p*'q = 0_. L by Th20; hence thesis by POLYNOM4:3; end; end; theorem Th34: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being Polynomial of L st p*'q is non-zero holds p is non-zero & q is non-zero proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p, q being Polynomial of L; assume that A1: p*'q is non-zero and A2: p is non non-zero or q is non non-zero; len p = 0 or len q = 0 by A2,Th17; then len (p*'q) = 0 by Th33; hence thesis by A1,Th17; end; theorem for L being add-associative right_zeroed right_complementable distributive commutative associative well-unital non empty doubleLoopStr, p, q being Polynomial of L st p.(len p -'1) * q.(len q -'1) <> 0.L holds 0 < len ( p*'q) proof let L be add-associative right_zeroed right_complementable distributive commutative associative well-unital non empty doubleLoopStr, p, q being Polynomial of L; assume A1: p.(len p -'1) * q.(len q -'1) <> 0.L; now assume len q <= 0; then len q = 0; then q = 0_. L by POLYNOM4:5; then q.(len q -'1) = 0.L by FUNCOP_1:7; hence contradiction by A1,VECTSP_1:6; end; then A2: 0 qua Nat+1 <= len q by NAT_1:13; now assume len p <= 0; then len p = 0; then p = 0_. L by POLYNOM4:5; then p.(len p -'1) = 0.L by FUNCOP_1:7; hence contradiction by A1,VECTSP_1:7; end; then 0 qua Nat+1 <= len p by NAT_1:13; then len p + len q >= 1+1 by A2,XREAL_1:7; then len p + len q -1 >= 1+1-1 by XREAL_1:9; hence thesis by A1,POLYNOM4:10; end; theorem Th36: for L being add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr, p, q being Polynomial of L st 1 < len p & 1 < len q holds len p < len (p*'q) proof let L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr, p, q be Polynomial of L such that A1: 1 < len p and A2: 1 < len q; p.(len p -'1) <> 0.L & q.(len q -'1)<>0.L by A1,A2,Th18; then p.(len p -'1) * q.(len q -'1)<>0.L by VECTSP_2:def 1; then A3: len (p*'q) = len p + len q - 1 by POLYNOM4:10; len q - 1 > 1-1 by A2,XREAL_1:14; then len p + (len q - 1) > 0 qua Nat+len p by XREAL_1:8; hence thesis by A3; end; theorem Th37: for L being add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, a, b being Element of L, p being Polynomial of L holds (<%a, b%>*'p).0 = a*p.0 & for i being Nat holds (<%a, b%> *'p).(i+1) = a*p.(i+1)+b*p.i proof let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, a, b be Element of L, q be Polynomial of L; set p = <%a, b%>; consider r being FinSequence of L such that A1: len r = 0 qua Nat+1 and A2: p*'q.0 = Sum r and A3: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(0 qua Nat+1-'k) by POLYNOM3:def 9; A4: 1 in dom r by A1,FINSEQ_3:25; then reconsider r1 = r.1 as Element of L by FINSEQ_2:11; r = <*r1*> by A1,FINSEQ_1:40; then Sum r = r1 by RLVECT_1:44 .= p.(1-'1) * q.(0 qua Nat+1-'1) by A3,A4 .= p.0 * q.(0 qua Nat+1-'1) by XREAL_1:232 .= p.0 * q.0 by NAT_D:34; hence (<%a, b%>*'q).0 = a*q.0 by A2,POLYNOM5:38; let i be Nat; consider r being FinSequence of L such that A5: len r = (i+1)+1 and A6: p*'q.(i+1) = Sum r and A7: for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.((i+1 )+1-'k) by POLYNOM3:def 9; len r = i+2 by A5; then A8: 0 qua Nat+2 <= len r by XREAL_1:6; then A9: 2 in dom r by FINSEQ_3:25; then A10: r/.2 = r.2 by PARTFUN1:def 6 .= p.(1+1-'1) * q.((i+1)+1-'2) by A7,A9 .= p.1 * q.((i+1)+1-'2) by NAT_D:34 .= b * q.(i+(1+1)-'2) by POLYNOM5:38 .= b * q.i by NAT_D:34; A11: now let k be Element of NAT such that A12: 2 < k and A13: k in dom r; consider k1 being Nat such that A14: k = k1+1 by A12,NAT_1:6; A15: 2 <= k1 by A12,A14,NAT_1:13; reconsider k1 as Element of NAT by ORDINAL1:def 12; thus r.k = p.(k-'1) * q.((i+1)+1-'k) by A7,A13 .= p.k1 * q.((i+1)+1-'k) by A14,NAT_D:34 .= (0.L) * q.((i+1)+1-'k) by A15,POLYNOM5:38 .= 0.L by VECTSP_1:7; end; 1 <= len r by A8,XXREAL_0:2; then A16: 1 in dom r by FINSEQ_3:25; then r/.1 = r.1 by PARTFUN1:def 6 .= p.(1-'1) * q.((i+1)+1-'1) by A7,A16 .= p.0 * q.((i+1)+1-'1) by XREAL_1:232 .= p.0 * q.(i+1) by NAT_D:34 .= a*q.(i+1) by POLYNOM5:38; hence thesis by A6,A8,A10,A11,Th2; end; theorem Th38: for L being add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r being Element of L, q being non-zero Polynomial of L holds len (<%r, 1.L%>*'q) = len q + 1 proof let L be add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r be Element of L, q being non-zero Polynomial of L; set p = <%r, 1.L%>; A1: p.(len p -'1) * q.(len q -'1) = p.(1+1-'1) * q.(len q -'1) by POLYNOM5:40 .= p.(1) * q.(len q -'1) by NAT_D:34 .= 1.L * q.(len q -'1) by POLYNOM5:38 .= q.(len q -'1) by VECTSP_1:def 8; len <%r, 1.L%> = 2 & len q > 0 by Th17,POLYNOM5:40; hence len (<%r, 1.L%>*'q) = len q +(1+1)-1 by A1,Th18,POLYNOM4:10 .= len q +1; end; theorem Th39: for L being non degenerated comRing, x being Element of L, i being Element of NAT holds len (<%x, 1.L%>`^i) = i+1 proof let L be non degenerated comRing, x be Element of L; defpred P[Element of NAT] means len (<%x, 1.L%>`^$1) = $1+1; set r = <%x, 1.L%>; A1: for i being Element of NAT st P[i] holds P[i+1] proof let i be Element of NAT such that A2: P[i]; reconsider ri = r`^i as non-zero Polynomial of L by A2,Th17; thus len (r`^(i+1)) = len ((r`^1)*'ri) by Th30 .= len (r*'ri) by POLYNOM5:16 .= i+1+1 by A2,Th38; end; r`^0 = 1_. L by POLYNOM5:15; then A3: P[ 0 ] by POLYNOM4:4; thus for i being Element of NAT holds P[i] from NAT_1:sch 1(A3,A1); end; registration let L be non degenerated comRing, x be Element of L, n be Element of NAT; cluster <%x, 1.L%>`^n -> non-zero; correctness proof len (<%x, 1.L%>`^n) = n+1 by Th39; hence thesis by Th17; end; end; theorem Th40: for L being non degenerated comRing, x being Element of L, q being non-zero (Polynomial of L), i being Element of NAT holds len ((<%x, 1.L%> `^i)*'q) = i + len q proof let L being non degenerated comRing, x being Element of L, q being non-zero Polynomial of L; set r = <%x, 1.L%>; defpred P[Element of NAT] means len ((r`^$1)*'q) = $1 + len q; A1: for i being Element of NAT st P[i] holds P[i+1] proof let i be Element of NAT such that A2: P[i]; len q > 0 by Th17; then A3: (r`^i)*'q is non-zero by A2,Th17; thus len ((r`^(i+1))*'q) = len ((r`^1)*'(r`^i)*'q) by Th30 .= len (r*'(r`^i)*'q) by POLYNOM5:16 .= len (r*'((r`^i)*'q)) by POLYNOM3:33 .= (i+len q)+1 by A2,A3,Th38 .= (i+1)+len q; end; len ((r`^0)*'q) = len ((1_. L)*'q) by POLYNOM5:15 .= 0 qua Nat+ len q by POLYNOM3:35; then A4: P[ 0 ]; thus for i being Element of NAT holds P[i] from NAT_1:sch 1(A4,A1); end; theorem Th41: for L being add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r being Element of L, p, q being Polynomial of L st p = <%r, 1. L%>*'q & p.(len p -'1) = 1.L holds q.(len q -'1) = 1.L proof let L be add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, x be Element of L, p, q be Polynomial of L such that A1: p = <%x, 1.L%>*'q and A2: p.(len p -'1) = 1.L; set lp1 = len p -'1; A3: now assume q = 0_. L; then p = 0_. L by A1,POLYNOM3:34; hence contradiction by A2,FUNCOP_1:7; end; then q is non-zero by Def5; then len p = len q + 1 by A1,Th38; then A4: lp1 = len q by NAT_D:34; then consider lp2 being Nat such that A5: lp1 = lp2+1 by A3,NAT_1:6,POLYNOM4:5; reconsider lp2 as Element of NAT by ORDINAL1:def 12; A6: q.lp1 = 0.L by A4,ALGSEQ_1:8; (<%x, 1.L%>*'q).lp1 = x*q.(lp1)+(1.L)*q.lp2 by A5,Th37 .= 0.L +(1.L)*q.lp2 by A6,VECTSP_1:6 .= (1.L)*q.lp2 by RLVECT_1:4 .= q.lp2 by VECTSP_1:def 8; hence thesis by A1,A2,A4,A5,NAT_D:34; end; begin :: Little Bezout theorem definition let L be non empty ZeroStr, p be Polynomial of L; let n be Nat; func poly_shift(p,n) -> Polynomial of L means :Def6: for i being Nat holds it.i = p.(n + i); existence proof deffunc F(Nat) = p.(n+$1); consider ps being AlgSequence of L such that A1: len ps <= len p and A2: for k being Nat st k < len p holds ps.k = F(k) from ALGSEQ_1:sch 1; take ps; let i be Nat; per cases; suppose i < len p; hence thesis by A2; end; suppose A3: i >= len p; hence ps.i = 0.L by A1,ALGSEQ_1:8,XXREAL_0:2 .= p.(n + i) by A3,ALGSEQ_1:8,NAT_1:12; end; end; uniqueness proof let it1, it2 be Polynomial of L such that A4: for i being Nat holds it1.i = p.(n + i) and A5: for i being Nat holds it2.i = p.(n + i); now let x be set; assume x in NAT; then reconsider i = x as Element of NAT; thus it1.x = p.(n+i) by A4 .= it2.x by A5; end; hence it1 = it2 by FUNCT_2:12; end; end; theorem Th42: for L being non empty ZeroStr,p being Polynomial of L holds poly_shift(p,0) = p proof let L be non empty ZeroStr, p be Polynomial of L; set ps = poly_shift(p,0); now let x be set; assume x in NAT; then reconsider i = x as Element of NAT; thus ps.x = p.(0 qua Nat+i) by Def6 .= p.x; end; hence thesis by FUNCT_2:12; end; theorem Th43: for L being non empty ZeroStr, n being Element of NAT, p being Polynomial of L st n >= len p holds poly_shift(p,n) = 0_. L proof let L be non empty ZeroStr, n be Element of NAT, p be Polynomial of L; set ps = poly_shift(p,n); assume A1: n >= len p; A2: now let z be set; assume z in dom ps; then reconsider i = z as Element of NAT; thus ps.z = p.(n+i) by Def6 .= 0.L by A1,ALGSEQ_1:8,NAT_1:12; end; dom ps = NAT by FUNCT_2:def 1; hence thesis by A2,FUNCOP_1:11; end; theorem Th44: for L being non degenerated non empty multLoopStr_0, n being Element of NAT, p being Polynomial of L st n <= len p holds len poly_shift(p,n) + n = len p proof let L be non degenerated non empty multLoopStr_0, n be Element of NAT, p be Polynomial of L such that A1: n <= len p; set ps = poly_shift(p,n), lpn = len p - n; n-n <= lpn by A1,XREAL_1:9; then reconsider lpn as Element of NAT by INT_1:3; A2: now let m be Nat such that A3: m is_at_least_length_of ps and A4: lpn > m; lpn >= m+1 by A4,NAT_1:13; then A5: lpn -1 >= m +1-1 by XREAL_1:9; then reconsider lpn1 = lpn -1 as Element of NAT by INT_1:3; (n+lpn1)+1 = len p; then A6: p.(n+lpn1) <> 0.L by ALGSEQ_1:10; ps.lpn1 = p.(n+lpn1) by Def6; hence contradiction by A3,A5,A6,ALGSEQ_1:def 2; end; now let i be Nat; assume i >= lpn; then A7: i+n >= len p by XREAL_1:20; thus ps.i = p.(n+i) by Def6 .= 0.L by A7,ALGSEQ_1:8; end; then lpn is_at_least_length_of ps by ALGSEQ_1:def 2; hence len poly_shift(p,n) + n = lpn + n by A2,ALGSEQ_1:def 3 .= len p; end; theorem Th45: for L being non degenerated comRing, x being Element of L, n being Element of NAT, p being Polynomial of L st n < len p holds eval( poly_shift(p,n),x) = x*eval(poly_shift(p,n+1),x) + p.n proof let L be non degenerated comRing, x being Element of L, n be Element of NAT, p being Polynomial of L such that A1: n < len p; set ps = poly_shift(p,n), ps1 = poly_shift(p,n+1); consider f be FinSequence of L such that A2: eval(ps,x) = Sum f and A3: len f = len ps and A4: for k be Element of NAT st k in dom f holds f.k = ps.(k-'1) * (power L).(x,k-'1) by POLYNOM4:def 2; consider f1 be FinSequence of L such that A5: eval(ps1,x) = Sum f1 and A6: len f1 = len ps1 and A7: for k be Element of NAT st k in dom f1 holds f1.k = ps1.(k-'1) * ( power L).(x,k-'1) by POLYNOM4:def 2; rng f1 c= the carrier of L & dom (x multfield) = the carrier of L by FUNCT_2:def 1; then A8: x*f1 = (x multfield)*f1 & dom ((x multfield)*f1) = dom f1 by FVSUM_1:def 6 ,RELAT_1:27; A9: 1_L = 1.L; now A10: n+1 <= len p by A1,NAT_1:13; A11: len ps1 +1+n = len ps1 + (n+1) .= len p by A10,Th44 .= len ps + n by A1,Th44; thus len f = len f; A12: len <*p.n*> = 1 by FINSEQ_1:40; A13: len ((x*f1)) = len f1 by A8,FINSEQ_3:29; hence len (<*p.n*>^(x*f1)) = len f by A3,A6,A11,A12,FINSEQ_1:22; let j be Nat such that A14: j in dom f; A15: 1 <= j by A14,FINSEQ_3:25; A16: j <= len f by A14,FINSEQ_3:25; per cases by A15,XXREAL_0:1; suppose A17: j = 1; A18: 1 in dom <*p.n*> by A12,FINSEQ_3:25; thus f.j = ps.(1-'1) * (power L).(x,1-'1) by A4,A14,A17 .= ps.0 * (power L).(x,1-'1) by XREAL_1:232 .= ps.0 * (power L).(x,0) by XREAL_1:232 .= ps.0 * 1.L by A9,GROUP_1:def 7 .= ps.0 by A9,GROUP_1:def 4 .= p.(n+(0 qua Nat)) by Def6 .= <*p.n*>.1 by FINSEQ_1:40 .= (<*p.n*>^(x*f1)).j by A17,A18,FINSEQ_1:def 7; end; suppose A19: 1 < j; 1-1 <= j-1 by A15,XREAL_1:9; then reconsider j1 = j-1 as Element of NAT by INT_1:3; A20: 1+1 <= j by A19,NAT_1:13; then A21: 1+1-1 <= j-1 by XREAL_1:9; then ex j2 being Nat st j1 = j2+1 by NAT_1:6; then A22: j1-'1+1 = j1 by NAT_D:34; j = j1+1; then A23: j1 = j-'1 by NAT_D:34; j-1 <= len f1 + 1-1 by A3,A6,A11,A16,XREAL_1:9; then A24: j1 in dom f1 by A21,FINSEQ_3:25; then reconsider f1j = f1.j1 as Element of L by FINSEQ_2:11; thus f.j = ps.(j-'1) * (power L).(x,j-'1) by A4,A14 .= p.(n+j1) * (power L).(x,j1) by A23,Def6 .= p.((n+1)+(j1-'1)) * (((power L).(x,j1-'1)) * x) by A22,GROUP_1:def 7 .= x*(p.((n+1)+(j1-'1)) * (power L).(x,j1-'1)) by GROUP_1:def 3 .= x*(ps1.(j1-'1) * (power L).(x,j1-'1)) by Def6 .= x*f1j by A7,A24 .= (x*f1).j1 by A8,A24,FVSUM_1:50 .= (<*p.n*>^(x*f1)).j by A3,A6,A11,A12,A13,A16,A20,FINSEQ_1:23; end; end; then x*(Sum f1) = Sum (x*f1) & f = <*p.n*>^(x*f1) by FINSEQ_2:9,FVSUM_1:73; hence thesis by A2,A5,FVSUM_1:72; end; theorem Th46: for L being non degenerated comRing, p being Polynomial of L st len p = 1 holds Roots p = {} proof let L be non degenerated comRing, p be Polynomial of L; assume len p = 1; then A1: p =<%p.0%> & p.0 <> 0.L by Th19; assume Roots p <> {}; then consider x being set such that A2: x in Roots p by XBOOLE_0:def 1; reconsider x as Element of L by A2; x is_a_root_of p by A2,POLYNOM5:def 9; then eval(p,x) = 0.L by POLYNOM5:def 6; hence contradiction by A1,POLYNOM5:37; end; definition let L be non degenerated comRing, r be Element of L, p be Polynomial of L such that A1: r is_a_root_of p; func poly_quotient(p,r) -> Polynomial of L means :Def7: len it + 1 = len p & for i being Nat holds it.i = eval(poly_shift(p, i+1),r) if len p > 0 otherwise it = 0_. L; existence proof hereby r in Roots p by A1,POLYNOM5:def 9; then A1: len p <> 1 by Th46; deffunc F(Nat) = eval(poly_shift(p, $1+1),r); set lq = len p -'1; consider q being sequence of L such that A2: for k being Element of NAT holds q.k = F(k) from FUNCT_2:sch 4; reconsider q as sequence of L; assume A3: len p > 0; then consider p1 being Nat such that A4: len p = p1+1 by NAT_1:6; A5: lq = p1 by A4,NAT_D:34; then A6: lq < len p by A4,NAT_1:13; len p >= 0 qua Nat+1 by A3,NAT_1:13; then consider lq1 being Nat such that A7: lq = lq1 + 1 by A4,A5,A1,NAT_1:6; A8: now let i be Nat; assume i >= lq; then i >= p1 by A4,NAT_D:34; then A9: i+1 >= len p by A4,XREAL_1:6; i in NAT by ORDINAL1:def 12; hence q.i = eval(poly_shift(p, i+1),r) by A2 .= eval(0_.L,r) by A9,Th43 .= 0.L by POLYNOM4:17; end; reconsider lq1 as Element of NAT by ORDINAL1:def 12; q.lq1 = eval(poly_shift(p, lq1+1),r) by A2 .= r*eval(poly_shift(p, len p),r) + p.lq by A4,A5,A7,A6,Th45 .= r*eval(0_. L,r) + p.lq by Th43 .= r*0.L + p.lq by POLYNOM4:17 .= 0.L + p.lq by VECTSP_1:6 .= p.lq by RLVECT_1:4; then A10: q.lq1 <> 0.L by A4,A5,ALGSEQ_1:10; reconsider q as AlgSequence of L by A8,ALGSEQ_1:def 1; A11: lq1 = lq -'1 by A7,NAT_D:34; A12: now let m be Nat; assume A13: m is_at_least_length_of q; assume A14: lq > m; then consider lq1 being Nat such that A15: lq = lq1 + 1 by NAT_1:6; lq1 >= m by A14,A15,NAT_1:13; then lq -'1 >= m by A15,NAT_D:34; hence contradiction by A11,A10,A13,ALGSEQ_1:def 2; end; take q; lq is_at_least_length_of q by A8,ALGSEQ_1:def 2; hence len q + 1 =p1+1-'1+1 by A4,A12,ALGSEQ_1:def 3 .=len p by A4,NAT_D:34; let k be Nat; k in NAT by ORDINAL1:def 12; hence q.k = F(k) by A2; end; thus thesis; end; uniqueness proof let it1, it2 be Polynomial of L; hereby assume len p > 0; assume that A16: len it1 + 1 = len p and A17: for i being Nat holds it1.i = eval(poly_shift(p, i+1),r) and A18: len it2 + 1 = len p and A19: for i being Nat holds it2.i = eval(poly_shift(p, i+1),r); now let k be Nat such that k < len it1; thus it1.k = eval(poly_shift(p, k+1),r) by A17 .= it2.k by A19; end; hence it1 = it2 by A16,A18,ALGSEQ_1:12; end; thus thesis; end; consistency; end; theorem Th47: for L being non degenerated comRing, r being Element of L, p being non-zero Polynomial of L st r is_a_root_of p holds len poly_quotient(p,r) > 0 proof let L be non degenerated comRing, r be Element of L, p be non-zero Polynomial of L such that A1: r is_a_root_of p; assume len poly_quotient(p,r) <= 0; then A2: len poly_quotient(p,r) = 0; len p > 0 by Th17; then len poly_quotient(p,r) + 1 = len p by A1,Def7; then Roots p = {} by A2,Th46; hence contradiction by A1,POLYNOM5:def 9; end; theorem Th48: for L being add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr, x being Element of L holds Roots <%-x, 1.L%> = {x} proof let L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr, x be Element of L; now let a be set; hereby assume A1: a in Roots <%-x, 1.L%>; then reconsider b = a as Element of L; b is_a_root_of <%-x, 1.L%> by A1,POLYNOM5:def 9; then 0.L = eval(<%-x, 1.L%>,b) by POLYNOM5:def 6 .= -x + b by POLYNOM5:47; then -x = -b by RLVECT_1:6; hence x = a by RLVECT_1:18; end; eval(<%-x, 1.L%>,x) = -x + x by POLYNOM5:47 .= 0.L by RLVECT_1:5; then A2: x is_a_root_of <%-x, 1.L%> by POLYNOM5:def 6; assume a = x; hence a in Roots <%-x, 1.L%> by A2,POLYNOM5:def 9; end; hence thesis by TARSKI:def 1; end; theorem Th49: for L being non trivial comRing, x being Element of L, p, q being Polynomial of L st p = <%-x,1.L%>*'q holds x is_a_root_of p proof let L be non trivial comRing, x be Element of L, p, q be Polynomial of L such that A1: p = <%-x,1.L%>*'q; A2: eval(<%-x,1.L%>,x) = (-x)+x by POLYNOM5:47 .= 0.L by RLVECT_1:5; thus eval(p,x) = eval(<%-x,1.L%>,x) * eval(q,x) by A1,POLYNOM4:24 .= 0.L by A2,VECTSP_1:7; end; ::$N Little Bezout Theorem (Factor Theorem) theorem Th50: :: Factor theorem (Bezout) for L being non degenerated comRing, r being Element of L, p being Polynomial of L st r is_a_root_of p holds p = <%-r,1.L%>*'poly_quotient(p ,r) proof let L be non degenerated comRing, x be Element of L, p be Polynomial of L; assume A1: x is_a_root_of p; set r = <%-x,1.L%>, pq = poly_quotient(p,x); per cases; suppose A2: len p > 0; r.(len r -'1) = r.(1+1-'1) by POLYNOM5:40 .= r.1 by NAT_D:34 .= 1.L by POLYNOM5:38; then A3: r.(len r -'1) * pq.(len pq -'1) = pq.(len pq -'1) by VECTSP_1:def 8; p is non-zero by A2,Th17; then A4: len pq > 0 by A1,Th47; now len (r *' pq) = len r + len pq - 1 by A4,A3,Th18,POLYNOM4:10 .= len pq +(1+1)-1 by POLYNOM5:40 .= len pq +1 .= len p by A1,A2,Def7; hence len p = len (r *' pq); defpred P[Nat] means p.$1 = (r*'pq).$1; let k be Nat; assume k < len p; A5: 0.L = eval(p,x) by A1,POLYNOM5:def 6 .= eval(poly_shift(p,0),x) by Th42 .= x*eval(poly_shift(p,0 qua Nat+1),x) + p.0 by A2,Th45; A6: (-x)*eval(poly_shift(p, 0 qua Nat+1),x) = (-x)*eval(poly_shift(p, 0 qua Nat+1),x) + 0.L by RLVECT_1:def 4 .= (-x)*eval(poly_shift(p, 0 qua Nat+1),x) + x*eval(poly_shift(p,1), x) + p.0 by A5,RLVECT_1:def 3 .= -x*eval(poly_shift(p, 0 qua Nat+1),x) + x*eval(poly_shift(p,1),x) + p.0 by VECTSP_1:9 .= 0.L +p.0 by RLVECT_1:5 .= p.0 by RLVECT_1:4; A7: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; A8: pq.(k+1) = eval(poly_shift(p, k+1+1),x) by A1,A2,Def7; A9: pq.k = eval(poly_shift(p, k+1),x) by A1,A2,Def7; per cases; suppose A10: k+1 >= len p; then A11: pq.(k+1) = eval(0_.L,x) by A8,Th43,NAT_1:12 .= 0.L by POLYNOM4:17; A12: pq.k = eval(0_.L,x) by A9,A10,Th43 .= 0.L by POLYNOM4:17; (r*'pq).(k+1) = (-x)*pq.(k+1)+(1.L)*pq.k by Th37 .= 0.L + (1.L)*pq.k by A11,VECTSP_1:6 .= 0.L + 0.L by A12,VECTSP_1:6 .= 0.L by RLVECT_1:4; hence thesis by A10,ALGSEQ_1:8; end; suppose k+1 < len p; then pq.k = x*eval(poly_shift(p, k+1+1),x) + p.(k+1) by A9,Th45; then A13: -x*pq.(k+1)+pq.k = -x*pq.(k+1)+x*eval(poly_shift(p, k+1+1),x)+p .(k+1) by RLVECT_1:def 3 .= 0.L + p.(k+1) by A8,RLVECT_1:5; (r*'pq).(k+1) = (-x)*pq.(k+1)+(1.L)*pq.k by Th37 .= (-x)*pq.(k+1)+pq.k by VECTSP_1:def 8 .= -x*pq.(k+1)+pq.k by VECTSP_1:9; hence thesis by A13,RLVECT_1:4; end; end; (r*'pq).0 = (-x)*pq.0 by Th37 .= (-x)*eval(poly_shift(p, 0 qua Nat+1),x) by A1,A2,Def7; then A14: P[ 0 ] by A6; for k being Nat holds P[k] from NAT_1:sch 2(A14,A7); hence p.k = (r*'pq).k; end; hence thesis by ALGSEQ_1:12; end; suppose len p = 0; then pq = 0_. L & p = 0_. L by A1,Def7,POLYNOM4:5; hence thesis by POLYNOM3:34; end; end; theorem :: Factor theorem (Bezout) for L being non degenerated comRing, r being Element of L, p, q being Polynomial of L st p = <%-r,1.L%>*'q holds r is_a_root_of p proof let L be non degenerated comRing, r be Element of L, p, q be Polynomial of L; assume p = <%-r,1.L%>*'q; then eval(p,r) = eval(<%-r,1.L%>,r) * eval(q,r) by POLYNOM4:24 .= (-r+r) * eval(q,r) by POLYNOM5:47 .= 0.L * eval(q,r) by RLVECT_1:def 10 .= 0.L by VECTSP_1:7; hence thesis by POLYNOM5:def 6; end; Lm1: now let L be domRing, p be non-zero Polynomial of L; defpred P[Nat] means for p being Polynomial of L st len p = $1 holds Roots p is finite & ex n being Element of NAT st n = card Roots p & n < len p; p <> 0_. L by Def5; then len p <> 0 by POLYNOM4:5; then A1: len p >= 0 qua Nat+1 by NAT_1:13; A2: for n being Nat st n>=1 & P[n] holds P[n+1] proof let n be Nat such that n >= 1 and A3: P[n]; let p be Polynomial of L; assume A4: len p = n+1; per cases; suppose p is with_roots; then consider x being Element of L such that A5: x is_a_root_of p by POLYNOM5:def 7; set r = <%-x,1.L%>, pq = poly_quotient(p,x); A6: p = <%-x,1.L%>*'poly_quotient(p,x) by A5,Th50; then A7: Roots p = (Roots r)\/Roots pq by Th23; A8: Roots r = {x} by Th48; then reconsider Rr = Roots r as finite set; A9: len pq + 1 = len p by A4,A5,Def7; then consider k being Element of NAT such that A10: k = card Roots pq and A11: k < len pq by A3,A4; reconsider Rpq = Roots pq as finite set by A3,A4,A9; reconsider Rp = Rpq \/ Rr as finite set; card Rr = 1 by A8,CARD_1:30; then A12: card Rp <= k + 1 by A10,CARD_2:43; Roots pq is finite by A3,A4,A9; hence Roots p is finite by A8,A7; take m = card Rp; thus m = card Roots p by A6,Th23; k+1 < n+1 by A4,A9,A11,XREAL_1:8; hence thesis by A4,A12,XXREAL_0:2; end; suppose A13: not p is with_roots; A14: now assume Roots p <> {}; then consider x being set such that A15: x in Roots p by XBOOLE_0:def 1; reconsider x as Element of L by A15; x is_a_root_of p by A15,POLYNOM5:def 9; hence contradiction by A13,POLYNOM5:def 7; end; hence Roots p is finite; take 0; thus 0 = card Roots p by A14; thus thesis by A4; end; end; A16: P[1] proof let p be Polynomial of L; assume A17: len p = 1; hence Roots p is finite by Th46; take 0; thus 0 = card Roots p by A17,Th46,CARD_1:27; thus thesis by A17; end; for n being Nat st n >= 1 holds P[n] from NAT_1:sch 8(A16,A2); hence Roots p is finite & ex n being Element of NAT st n = card Roots p & n < len p by A1; end; begin :: Polynomials defined by roots registration let L be domRing, p be non-zero Polynomial of L; cluster Roots p -> finite; correctness by Lm1; end; definition let L be non degenerated comRing, x be Element of L, p be non-zero ( Polynomial of L); func multiplicity(p,x) -> Element of NAT means :Def8: ex F being finite non empty Subset of NAT st F = {k where k is Element of NAT : ex q being Polynomial of L st p = (<%-x, 1.L%>`^k) *' q} & it = max F; existence proof set r = <%-x, 1.L%>; defpred P[Element of NAT] means ex q being Polynomial of L st p = (r`^$1) *' q; set F = {k where k is Element of NAT : P[k]}; A1: F c= NAT from FRAENKEL:sch 10; p = (1_. L) *' p by POLYNOM3:35 .= (r`^0) *' p by POLYNOM5:15; then A2: 0 in F; A3: len p > 0 by Th17; F c= len p proof let a be set; assume a in F; then consider k being Element of NAT such that A4: a = k and A5: P[k]; consider q being Polynomial of L such that A6: p = (r`^k) *' q by A5; A7: now assume len q = 0; then q = 0_. L by POLYNOM4:5; then p = 0_. L by A6,POLYNOM4:2; hence contradiction by A3,POLYNOM4:3; end; then reconsider q as non-zero Polynomial of L by Th17; now assume k >= len p; then k+len q > len p + (0 qua Nat) by A7,XREAL_1:8; hence contradiction by A6,Th40; end; then k in {i where i is Element of NAT : i < len p}; hence thesis by A4,AXIOMS:4; end; then reconsider F as finite non empty Subset of NAT by A2,A1; reconsider FF = F as finite non empty natural-membered set; reconsider m = max FF as Element of NAT by ORDINAL1:def 12; take m; thus thesis; end; uniqueness; end; theorem Th52: for L being non degenerated comRing, p being non-zero ( Polynomial of L), x being Element of L holds x is_a_root_of p iff multiplicity( p,x) >= 1 proof let L be non degenerated comRing, p being non-zero (Polynomial of L), x being Element of L; set r = <%-x, 1.L%>; set m = multiplicity(p,x); consider F being finite non empty Subset of NAT such that A1: F = {k where k is Element of NAT : ex q being Polynomial of L st p = (r`^k) *' q} and A2: m = max F by Def8; m in F by A2,XXREAL_2:def 8; then consider k being Element of NAT such that A3: m = k and A4: ex q being Polynomial of L st p = (r`^k) *' q by A1; hereby assume x is_a_root_of p; then A5: p = r*'poly_quotient(p,x) by Th50; r`^1 = r by POLYNOM5:16; then 1 in F by A1,A5; hence multiplicity(p,x) >= 1 by A2,XXREAL_2:def 8; end; consider q being Polynomial of L such that A6: p = (r`^k) *' q by A4; assume multiplicity(p,x) >= 1; then consider k1 being Nat such that A7: k = k1+1 by A3,NAT_1:6; reconsider k1 as Element of NAT by ORDINAL1:def 12; p = r *' (r`^k1) *' q by A6,A7,POLYNOM5:19 .= r *' ((r`^k1) *' q) by POLYNOM3:33; hence thesis by Th49; end; theorem Th53: for L being non degenerated comRing, x being Element of L holds multiplicity(<%-x, 1.L%>,x) = 1 proof let L be non degenerated comRing, x be Element of L; set r = <%-x, 1.L%>; set j = multiplicity(r,x); consider F being finite non empty Subset of NAT such that A1: F = {k where k is Element of NAT : ex q being Polynomial of L st r = (r`^k) *' q} and A2: multiplicity(r,x) = max F by Def8; j in F by A2,XXREAL_2:def 8; then consider k being Element of NAT such that A3: k = j and A4: ex q being Polynomial of L st r = (r`^k) *' q by A1; consider q being Polynomial of L such that A5: r = (r`^k) *' q by A4; A6: len r = 2 by POLYNOM5:40; A7: now assume len q = 0; then q = 0_. L by POLYNOM4:5; then r = 0_. L by A5,POLYNOM4:2; hence contradiction by A6,POLYNOM4:3; end; then A8: q is non-zero by Th17; A9: now assume k > 1; then k >= 1+1 by NAT_1:13; then k+len q > 2+(0 qua Nat) by A7,XREAL_1:8; hence contradiction by A6,A5,A8,Th40; end; r = (r`^1) by POLYNOM5:16; then r = (r`^1) *' 1_. L by POLYNOM3:35; then 1 in F by A1; then multiplicity(r,x) >= 1 by A2,XXREAL_2:def 8; hence thesis by A3,A9,XXREAL_0:1; end; definition let L be domRing, p be non-zero Polynomial of L; func BRoots(p) -> bag of the carrier of L means :Def9: support it = Roots p & for x being Element of L holds it.x = multiplicity(p,x); existence proof deffunc F(Element of L) = multiplicity(p,$1); consider b being Function of the carrier of L, NAT such that A1: for x being Element of L holds b.x = F(x) from FUNCT_2:sch 4; dom b = the carrier of L by FUNCT_2:def 1; then A2: support b c= the carrier of L by PRE_POLY:37; A3: now let x be set; hereby assume A4: x in support b; then reconsider xx = x as Element of L by A2; b.x <> 0 by A4,PRE_POLY:def 7; then A5: b.xx >= 0 qua Nat+1 by NAT_1:13; b.x = F(xx) by A1; then xx is_a_root_of p by A5,Th52; hence x in Roots p by POLYNOM5:def 9; end; assume A6: x in Roots p; then reconsider xx = x as Element of L; xx is_a_root_of p by A6,POLYNOM5:def 9; then multiplicity(p,xx) >= 1 by Th52; then b.xx >= 1 by A1; hence x in support b by PRE_POLY:def 7; end; then support b = Roots p by TARSKI:1; then reconsider b as bag of the carrier of L by PRE_POLY:def 8; take b; thus thesis by A1,A3,TARSKI:1; end; uniqueness proof let it1, it2 be bag of the carrier of L such that support it1 = Roots p and A7: for x being Element of L holds it1.x = multiplicity(p,x) and support it2 = Roots p and A8: for x being Element of L holds it2.x = multiplicity(p,x); now let x be set; assume x in the carrier of L; then reconsider xx = x as Element of L; thus it1.x = multiplicity(p,xx) by A7 .= it2.x by A8; end; hence it1 = it2 by PBOOLE:3; end; end; theorem Th54: for L being domRing, x being Element of L holds BRoots <%-x, 1.L %> = ({x}, 1)-bag proof let L be domRing, x be Element of L; set r = <%-x, 1.L%>; Roots r = {x} by Th48; then A1: support BRoots r = {x} by Def9; A2: x in {x} by TARSKI:def 1; now let i be set; assume i in the carrier of L; then reconsider i1 = i as Element of L; per cases; suppose A3: i = x; thus (BRoots r).i = multiplicity(r,i1) by Def9 .= 1 by A3,Th53 .= (({x}, 1)-bag).i by A2,A3,Th7; end; suppose i <> x; then A4: not i in {x} by TARSKI:def 1; hence (BRoots r).i = 0 by A1,PRE_POLY:def 7 .= (({x}, 1)-bag).i by A4,Th6; end; end; hence thesis by PBOOLE:3; end; theorem Th55: for L being domRing, x be Element of L, p, q being non-zero Polynomial of L holds multiplicity(p*'q,x) = multiplicity(p,x) + multiplicity(q ,x) proof let L be domRing,x be Element of L, p, q being non-zero Polynomial of L; set r = <%-x, 1.L%>; consider F being finite non empty Subset of NAT such that A1: F = {k where k is Element of NAT : ex pqq being Polynomial of L st p *'q = (r`^k) *' pqq} and A2: multiplicity(p*'q,x) = max F by Def8; consider f being finite non empty Subset of NAT such that A3: f = {k where k is Element of NAT : ex pq being Polynomial of L st p = (r`^k) *' pq} and A4: multiplicity(p,x) = max f by Def8; max f in f by XXREAL_2:def 8; then consider i being Element of NAT such that A5: i = max f and A6: ex pq being Polynomial of L st p = (r`^i) *' pq by A3; consider pq being Polynomial of L such that A7: p = (r`^i) *' pq by A6; consider g being finite non empty Subset of NAT such that A8: g = {k where k is Element of NAT : ex qq being Polynomial of L st q = (r`^k) *' qq} and A9: multiplicity(q,x) = max g by Def8; max F in F by XXREAL_2:def 8; then consider k being Element of NAT such that A10: k = max F and A11: ex pqq being Polynomial of L st p*'q = (r`^k) *' pqq by A1; consider pqq being Polynomial of L such that A12: p*'q = (r`^k) *' pqq by A11; max g in g by XXREAL_2:def 8; then consider j being Element of NAT such that A13: j = max g and A14: ex qq being Polynomial of L st q = (r`^j) *' qq by A8; consider qq being Polynomial of L such that A15: q = (r`^j) *' qq by A14; A16: p*'q = (r`^i) *' pq *' (r`^j) *' qq by A7,A15,POLYNOM3:33 .= (r`^i) *' (r`^j) *' pq *' qq by POLYNOM3:33 .= (r`^(i+j)) *' pq *' qq by Th30 .= (r`^(i+j)) *' (pq *' qq) by POLYNOM3:33; A17: now assume i+j < k; then 0 qua Nat+(i+j) < k; then A18: 0 < k-(i+j) by XREAL_1:20; then reconsider kij = k-(i+j) as Element of NAT by INT_1:3; consider kk being Nat such that A19: kij = kk+1 by A18,NAT_1:6; reconsider kk as Element of NAT by ORDINAL1:def 12; (r`^kij) = (r`^1) *' (r`^kk) by A19,Th30 .= r *' (r`^kk) by POLYNOM5:16; then A20: (r`^kij) *' pqq = r *' ((r`^kk) *' pqq) by POLYNOM3:33; (0_. L).1 = 0.L & r.1 = 1.L by FUNCOP_1:7,POLYNOM5:38; then A21: r`^(i+j) <> 0_. L by Th29; k = kij + (i+j); then p*'q = ((r`^(i+j)) *' (r`^kij)) *' pqq by A12,Th30 .= (r`^(i+j)) *' ((r`^kij) *' pqq) by POLYNOM3:33; then x is_a_root_of (pq *' qq) by A16,A21,A20,Th28,Th49; then x in Roots (pq *' qq) by POLYNOM5:def 9; then A22: x in (Roots pq \/ Roots qq) by Th23; per cases by A22,XBOOLE_0:def 3; suppose x in Roots(pq); then x is_a_root_of pq by POLYNOM5:def 9; then pq = r *' poly_quotient(pq,x) by Th50; then p = (r`^i) *' r *' poly_quotient(pq,x) by A7,POLYNOM3:33 .= (r`^i) *' (r`^1) *' poly_quotient(pq,x) by POLYNOM5:16 .= (r`^(i+1)) *' poly_quotient(pq,x) by Th30; then i+1 in f by A3; then i+1 <= i by A5,XXREAL_2:def 8; hence contradiction by NAT_1:13; end; suppose x in Roots(qq); then x is_a_root_of qq by POLYNOM5:def 9; then qq = r *' poly_quotient(qq,x) by Th50; then q = (r`^j) *' r *' poly_quotient(qq,x) by A15,POLYNOM3:33 .= (r`^j) *' (r`^1) *' poly_quotient(qq,x) by POLYNOM5:16 .= (r`^(j+1)) *' poly_quotient(qq,x) by Th30; then j+1 in g by A8; then j+1 <= j by A13,XXREAL_2:def 8; hence contradiction by NAT_1:13; end; end; i+j in F by A1,A16; then i+j <= k by A10,XXREAL_2:def 8; hence thesis by A2,A4,A9,A10,A5,A13,A17,XXREAL_0:1; end; theorem Th56: for L being domRing, p, q being non-zero Polynomial of L holds BRoots(p*'q) = BRoots(p) + BRoots(q) proof let L be domRing, p, q being non-zero Polynomial of L; now let i be set; assume i in the carrier of L; then reconsider x = i as Element of L; thus (BRoots(p*'q)).i = multiplicity(p*'q, x) by Def9 .= multiplicity(p,x) + multiplicity(q,x) by Th55 .= (BRoots p).i + multiplicity(q,x) by Def9 .= (BRoots p).i + (BRoots q).i by Def9 .= (BRoots(p) + BRoots(q)).i by PRE_POLY:def 5; end; hence thesis by PBOOLE:3; end; Lm2: now let L be domRing, p, q be non-zero Polynomial of L; BRoots(p*'q) = BRoots(p) + BRoots(q) by Th56; hence degree BRoots (p*'q) = degree (BRoots p) + degree BRoots q by Th15; end; theorem Th57: for L being domRing, p being non-zero Polynomial of L st len p = 1 holds degree BRoots p = 0 proof let L be domRing, p being non-zero Polynomial of L; assume len p = 1; then Roots p = {} by Th46; then support BRoots p = {} by Def9; then BRoots p = EmptyBag the carrier of L by BAGORDER:19; hence thesis by Th11; end; theorem Th58: for L being domRing, x be Element of L, n being Element of NAT holds degree BRoots (<%-x, 1.L%>`^n) = n proof let L be domRing, x be Element of L; set r = <%-x, 1.L%>; defpred P[Element of NAT] means degree BRoots (r`^$1) = $1; A1: for n being Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT such that A2: P[n]; r`^(n+1) = (r`^n)*'r by POLYNOM5:19; then A3: degree BRoots(r`^(n+1)) = degree BRoots (r`^n) + degree BRoots r by Lm2 .= n + degree ({x},1)-bag by A2,Th54; card {x} = 1 by CARD_1:30; hence thesis by A3,Th13; end; len 1_. L = 1 & r`^0 = 1_. L by POLYNOM4:4,POLYNOM5:15; then A4: P[ 0 ] by Th57; thus for n being Element of NAT holds P[n] from NAT_1:sch 1(A4, A1); end; theorem for L being algebraic-closed domRing, p being non-zero Polynomial of L holds degree BRoots p = len p -' 1 proof let L be algebraic-closed domRing, p be non-zero Polynomial of L; defpred P[Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 > 0 holds degree BRoots p = len p -' 1; A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k] proof let k be Nat; assume A2: for n being Nat st n < k holds P[n]; let p be non-zero Polynomial of L; assume that A3: len p = k and A4: k > 0; A5: k >= 0 qua Nat+1 by A4,NAT_1:13; thus thesis proof per cases by A5,XXREAL_0:1; suppose A6: k = 1; hence degree BRoots p = 1-1 by A3,Th57 .= len p -' 1 by A3,A6,XREAL_1:233; end; suppose A7: k > 1; then p is with_roots by A3,POLYNOM5:def 8; then consider x being Element of L such that A8: x is_a_root_of p by POLYNOM5:def 7; A9: multiplicity(p,x) >= 1 by A8,Th52; set r = <%-x, 1.L%>; consider F being finite non empty Subset of NAT such that A10: F = {l where l is Element of NAT : ex q being Polynomial of L st p = (<%-x, 1.L%>`^l) *' q} and A11: multiplicity(p,x) = max F by Def8; max F in F by XXREAL_2:def 8; then consider l being Element of NAT such that A12: l = max F and A13: ex q being Polynomial of L st p = (<%-x, 1.L%>`^l) *' q by A10; set rr = <%-x, 1.L%>`^l; consider q being Polynomial of L such that A14: p = (<%-x, 1.L%>`^l) *' q by A13; reconsider q as non-zero Polynomial of L by A14,Th34; len q > 0 by Th17; then A15: len q >= 0 qua Nat+1 by NAT_1:13; thus thesis proof len q > 0 by Th17; then A16: q.(len q -'1) <> 0.L by Th18; len rr > 0 by Th17; then rr.(len rr -'1) <> 0.L by Th18; then A17: rr.(len rr -'1) * q.(len q -'1) <> 0.L by A16,VECTSP_2:def 1; A18: l*2 -l+1 = l+1; A19: len r = 2 by POLYNOM5:40; then A20: len rr = l*2 -l+1 by POLYNOM5:23; then A21: len rr > 1 by A9,A11,A12,NAT_1:13; per cases by A15,XXREAL_0:1; suppose A22: len q = 1; A23: len p = len rr + len q -1 by A14,A17,POLYNOM4:10 .= len rr by A22; thus degree BRoots p = degree (BRoots rr) + degree BRoots q by A14 ,Lm2 .= degree (BRoots rr) + (0 qua Nat) by A22,Th57 .= 2*l-l+1-1 by Th58 .= len p -' 1 by A3,A5,A20,A23,XREAL_1:233; end; suppose A24: len q > 1; then A25: degree BRoots rr = l+1 -' 1 & degree BRoots q = len q -' 1 by A2,A3 ,A14,A20,A21,Th36; thus degree BRoots p = degree (BRoots rr) + degree BRoots q by A14 ,Lm2 .= len rr-'1 + (len q -'1) by A19,A18,A25,POLYNOM5:23 .= len rr-1 + (len q -'1) by A21,XREAL_1:233 .= len rr-1 + (len q -1) by A24,XREAL_1:233 .= len rr + len q -1 -1 .= len p -1 by A14,A17,POLYNOM4:10 .= len p -' 1 by A3,A7,XREAL_1:233; end; end; end; end; end; A26: for n being Nat holds P[n] from NAT_1:sch 4(A1); len p > 0 by Th17; hence thesis by A26; end; definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c be Element of L, n be Element of NAT; func fpoly_mult_root(c,n) -> FinSequence of Polynom-Ring L means :Def10: len it = n & for i being Element of NAT st i in dom it holds it.i = <% -c, 1.L%>; existence proof <% -c, 1.L%> is Element of Polynom-Ring L by POLYNOM3:def 10; then reconsider f = n |-> <% -c, 1.L%> as FinSequence of Polynom-Ring L by FINSEQ_2:63; take f; thus A1: len f = n by CARD_1:def 7; let i be Element of NAT; assume i in dom f; then i in Seg n by A1,FINSEQ_1:def 3; hence thesis by FUNCOP_1:7; end; uniqueness proof let it1, it2 be FinSequence of Polynom-Ring L such that A2: len it1 = n and A3: for i being Element of NAT st i in dom it1 holds it1.i = <% -c, 1. L%> and A4: len it2 = n and A5: for i being Element of NAT st i in dom it2 holds it2.i = <% -c, 1. L%>; A6: dom it1 = dom it2 by A2,A4,FINSEQ_3:29; now let x be Nat; assume A7: x in dom it1; hence it1.x = <% -c, 1.L%> by A3 .= it2.x by A5,A6,A7; end; hence thesis by A6,FINSEQ_1:13; end; end; definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L; func poly_with_roots(b) -> Polynomial of L means :Def11: ex f being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L st len f = card support b & s = canFS(support b) & (for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))) & it = Product FlattenSeq f; existence proof support b c= dom b & dom b = the carrier of L by PARTFUN1:def 2,PRE_POLY:37 ; then rng canFS(support b) c= the carrier of L by XBOOLE_1:1; then reconsider s = canFS(support b) as FinSequence of L by FINSEQ_1:def 4; deffunc F(set) = fpoly_mult_root(s/.$1,b.(s/.$1)); consider f being FinSequence such that A1: len f = card support b and A2: for k being Nat st k in dom f holds f.k = F(k) from FINSEQ_1:sch 2; rng f c= (the carrier of Polynom-Ring L)* proof let x be set; assume x in rng f; then consider i being Nat such that A3: i in dom f & f.i = x by FINSEQ_2:10; x = F(i) by A2,A3; hence thesis by FINSEQ_1:def 11; end; then reconsider f as FinSequence of (the carrier of Polynom-Ring L)* by FINSEQ_1:def 4; reconsider it1 = Product FlattenSeq f as Polynomial of L by POLYNOM3:def 10 ; take it1, f, s; thus len f = card support b by A1; thus s = canFS(support b); thus for i be Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/. i,b.(s/.i)) by A2; thus thesis; end; uniqueness proof let it1, it2 be Polynomial of L; given f1 being FinSequence of (the carrier of Polynom-Ring L)*, s1 being FinSequence of L such that A4: len f1 = card support b and A5: s1 = canFS(support b) and A6: for i being Element of NAT st i in dom f1 holds f1.i = fpoly_mult_root(s1/.i,b.(s1/.i)) and A7: it1 = Product FlattenSeq f1; given f2 being FinSequence of (the carrier of Polynom-Ring L)*, s2 being FinSequence of L such that A8: len f2 = card support b and A9: s2 = canFS(support b) & for i being Element of NAT st i in dom f2 holds f2.i = fpoly_mult_root(s2/.i,b.(s2/.i)) and A10: it2 = Product FlattenSeq f2; A11: dom f1 = dom f2 by A4,A8,FINSEQ_3:29; now let i be Nat; assume A12: i in dom f1; hence f1.i = fpoly_mult_root(s1/.i,b.(s1/.i)) by A6 .= f2.i by A5,A9,A11,A12; end; hence thesis by A4,A7,A8,A10,FINSEQ_2:9; end; end; theorem Th60: for L being Abelian add-associative right_zeroed right_complementable commutative distributive well-unital non empty doubleLoopStr holds poly_with_roots(EmptyBag the carrier of L) = <%1.L%> proof let L be Abelian add-associative right_zeroed right_complementable commutative distributive well-unital non empty doubleLoopStr; set b = EmptyBag the carrier of L; consider f being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L such that A1: len f = card support b and s = canFS(support b) and for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/. i,b.(s/.i)) and A2: poly_with_roots(b) = Product FlattenSeq f by Def11; f = <*>((the carrier of Polynom-Ring L)*) by A1,BAGORDER:18,CARD_1:27; then 1_Polynom-Ring L = 1.Polynom-Ring L & FlattenSeq f = <*>(the carrier of Polynom-Ring L); then Product FlattenSeq f = 1.Polynom-Ring L by GROUP_4:8 .= 1_.(L) by POLYNOM3:36; hence thesis by A2,Th31; end; theorem Th61: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c being Element of L holds poly_with_roots(({c},1)-bag) = <% -c, 1.L %> proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c being Element of L; set b = ({c},1)-bag; consider f being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L such that A1: len f = card support b and A2: s = canFS(support b) and A3: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root (s/.i,b.(s/.i)) and A4: poly_with_roots(b) = Product FlattenSeq f by Def11; A5: support b = {c} by Th8; then A6: s = <* c *> by A2,Th4; A7: card support b = 1 by A5,CARD_1:30; then A8: 1 in dom f by A1,FINSEQ_3:25; then A9: f.1 = f/.1 by PARTFUN1:def 6; len s = 1 by A2,A7,Th3; then 1 in dom s by FINSEQ_3:25; then A10: s/.1 = s.1 by PARTFUN1:def 6 .= c by A6,FINSEQ_1:40; set f1 = fpoly_mult_root(s/.1,b.(s/.1)); c in {c} by TARSKI:def 1; then b.(s/.1) = 1 by A10,Th7; then A11: len f1 = 1 by Def10; then A12: 1 in dom f1 by FINSEQ_3:25; f = <*f/.1*> by A1,A5,CARD_1:30,FINSEQ_5:14; then A13: FlattenSeq f = f.1 by A9,PRE_POLY:1; A14: f.1 = fpoly_mult_root(s/.1,b.(s/.1)) by A3,A8; f1 = <*f1/.1*> by A11,FINSEQ_5:14; hence poly_with_roots(({c},1)-bag) = f1/.1 by A4,A13,A14,FINSOP_1:11 .= f1.1 by A12,PARTFUN1:def 6 .= <% -c, 1.L %> by A10,A12,Def10; end; theorem Th62: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b being bag of the carrier of L, f being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L st len f = card support b & s = canFS(support b) & (for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))) holds len FlattenSeq f = degree b proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b being bag of the carrier of L, f being FinSequence of ( the carrier of Polynom-Ring L)*, s being FinSequence of L such that A1: len f = card support b and A2: s = canFS(support b) and A3: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root (s/.i,b.(s/.i)); reconsider Cf = Card f as FinSequence of NAT; consider g being FinSequence of NAT such that A4: degree b = Sum g and A5: g = b*canFS(support b) by Def4; len s = card support b by A2,Th3; then A6: dom f = dom s by A1,FINSEQ_3:29; A7: now A8: rng s c= dom b proof let x be set; assume x in rng s; then A9: x in support b by A2,FUNCT_2:def 3; support b c= dom b by PRE_POLY:37; hence thesis by A9; end; thus dom Card f = dom f by CARD_3:def 2 .= dom g by A2,A6,A5,A8,RELAT_1:27; let i be Nat; assume i in dom Card f; then A10: i in dom f by CARD_3:def 2; then A11: g.i = b.(s.i) by A2,A6,A5,FUNCT_1:13; f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A3,A10; then A12: len (f.i) = b.(s/.i) by Def10; thus Cf.i = card (f.i) by A10,CARD_3:def 2 .= g.i by A6,A10,A12,A11,PARTFUN1:def 6; end; len FlattenSeq f = Sum Cf by PRE_POLY:27; hence thesis by A4,A7,FINSEQ_1:13; end; theorem Th63: for L being add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b being bag of the carrier of L, f being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L , c being Element of L st len f = card support b & s = canFS(support b) & (for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i)) ) holds (c in support b implies card ((FlattenSeq f)"{<% -c, 1.L%>}) = b.c) & ( not c in support b implies card ((FlattenSeq f)"{<% -c, 1.L%>}) = 0) proof let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L, f be FinSequence of (the carrier of Polynom-Ring L)*, s be FinSequence of L, c be Element of L such that A1: len f = card support b and A2: s = canFS(support b) and A3: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root (s/.i,b.(s/.i)); len f = len s by A1,A2,Th3; then A4: dom f = dom s by FINSEQ_3:29; hereby set X = { k where k is Element of NAT : k < b.c }; set ff = FlattenSeq f; set Y = ff"{<% -c, 1.L%>}; assume c in support b; then c in rng s by A2,FUNCT_2:def 3; then consider i being Nat such that A5: i in dom s and A6: s.i = c by FINSEQ_2:10; defpred P[set,set] means ex n being Element of NAT st n = $1 & $2 = (Sum Card(f|(i-'1)))+(1+n); A7: for x being set st x in X ex y being set st P[x,y] proof let x be set; assume x in X; then consider k being Element of NAT such that A8: x = k and k < b.c; take (Sum Card(f|(i-'1)))+(1+k); thus thesis by A8; end; consider g being Function such that A9: dom g = X and A10: for x being set st x in X holds P[x,g.x] from CLASSES1:sch 1(A7); A11: s/.i = c by A5,A6,PARTFUN1:def 6; now let y be set; A12: <% -c, 1.L%>.0 = -c by POLYNOM5:38; hereby assume y in rng g; then consider x being set such that A13: x in dom g and A14: y = g.x by FUNCT_1:def 3; consider n being Element of NAT such that A15: n = x and A16: g.x = (Sum Card(f|(i-'1)))+(1+n) by A9,A10,A13; ex k being Element of NAT st x = k & k < b.c by A9,A13; then A17: 1 <= 1+n & 1+n <= b.c by A15,NAT_1:12,13; A18: f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A3,A4,A5; then len (f.i) = b.c by A11,Def10; then A19: 1+n in dom (f.i) by A17,FINSEQ_3:25; then (f.i).(1+n) = <% -c, 1.L%> by A11,A18,Def10; then A20: (f.i).(1+n) in {<% -c, 1.L%>} by TARSKI:def 1; (Sum Card (f|(i-'1))) + (1+n) in dom ff & (f.i).(1+n) = ff.((Sum Card (f|(i -'1))) + (1+n)) by A4,A5,A19,PRE_POLY:30; hence y in Y by A14,A16,A20,FUNCT_1:def 7; end; assume A21: y in Y; then reconsider yn = y as Element of NAT; A22: ff.y in {<% -c, 1.L%>} by A21,FUNCT_1:def 7; y in dom ff by A21,FUNCT_1:def 7; then consider i1, j being Element of NAT such that A23: i1 in dom f and A24: j in dom (f.i1) and A25: yn = (Sum Card (f|(i1-'1))) + j and A26: (f.i1).j = ff.yn by PRE_POLY:29; A27: f.i1 = fpoly_mult_root(s/.i1,b.(s/.i1)) by A3,A23; then (f.i1).j = <%-s/.i1, 1.L%> by A24,Def10; then <% -c, 1.L%> = <%-s/.i1, 1.L%> by A22,A26,TARSKI:def 1; then A28: c = s/.i1 by A12,POLYNOM5:38,RLVECT_1:18; i1 in dom s & s/.i1 = s.i1 by A4,A23,PARTFUN1:def 6; then A29: i1 = i by A2,A5,A6,A28,FUNCT_1:def 4; consider j1 being Nat such that A30: j = j1 + 1 by A24,FINSEQ_3:24,NAT_1:6; reconsider j1 as Element of NAT by ORDINAL1:def 12; len (f.i1) = b.c by A27,A28,Def10; then j <= b.c by A24,FINSEQ_3:25; then j1 < b.c by A30,NAT_1:13; then A31: j1 in X; then ex n being Element of NAT st n = j1 & g.j1 = (Sum Card(f |(i-'1)))+( 1+n) by A10; hence y in rng g by A9,A25,A30,A29,A31,FUNCT_1:3; end; then A32: rng g = Y by TARSKI:1; g is one-to-one proof let x1,x2 be set such that A33: x1 in dom g & x2 in dom g and A34: g.x1 = g.x2; (ex n1 being Element of NAT st n1 = x1 & g.x1 = (Sum Card (f|(i-'1) ))+(1+n1) )& ex n2 being Element of NAT st n2 = x2 & g.x2 = (Sum Card (f|(i-'1) ))+(1+ n2) by A9,A10,A33; hence thesis by A34; end; then b.c = { k where k is Element of NAT : k < b.c } & X,Y are_equipotent by A9,A32,AXIOMS:4,WELLORD2:def 4; hence card ((FlattenSeq f)"{<% -c, 1.L%>}) = b.c by CARD_1:def 2; end; assume that A35: not c in support b and A36: card ((FlattenSeq f)"{<% -c, 1.L%>}) <> 0; consider x being set such that A37: x in (FlattenSeq f)"{<% -c, 1.L%>} by A36,CARD_1:27,XBOOLE_0:def 1; A38: x in dom FlattenSeq f by A37,FUNCT_1:def 7; reconsider x as Element of NAT by A37; consider i, j being Element of NAT such that A39: i in dom f and A40: j in dom (f.i) and x = (Sum Card (f|(i-'1))) + j and A41: (f.i).j = (FlattenSeq f).x by A38,PRE_POLY:29; A42: s/.i = s.i & s.i in rng s by A4,A39,FUNCT_1:3,PARTFUN1:def 6; (FlattenSeq f).x in {<% -c, 1.L%>} by A37,FUNCT_1:def 7; then A43: (FlattenSeq f).x = <% -c, 1.L%> by TARSKI:def 1; f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A3,A39; then A44: (f.i).j = <% -s/.i, 1.L%> by A40,Def10; <% -c, 1.L%>.0 = -c by POLYNOM5:38; then c = s/.i by A41,A43,A44,POLYNOM5:38,RLVECT_1:18; hence contradiction by A2,A35,A42,FUNCT_2:def 3; end; theorem Th64: for L being comRing for b1,b2 being bag of the carrier of L holds poly_with_roots(b1+b2) = (poly_with_roots b1)*'(poly_with_roots b2) proof let L be comRing, b1,b2 be bag of the carrier of L; set b = b1+b2; A1: support b = support b1 \/ support b2 by PRE_POLY:38; consider f2 being FinSequence of (the carrier of Polynom-Ring L)*, s2 being FinSequence of L such that A2: len f2 = card support b2 and A3: s2 = canFS(support b2) and A4: for i being Element of NAT st i in dom f2 holds f2.i = fpoly_mult_root(s2/.i,b2.(s2/.i)) and A5: poly_with_roots(b2) = Product FlattenSeq f2 by Def11; consider f1 being FinSequence of (the carrier of Polynom-Ring L)*, s1 being FinSequence of L such that A6: len f1 = card support b1 and A7: s1 = canFS(support b1) and A8: for i being Element of NAT st i in dom f1 holds f1.i = fpoly_mult_root(s1/.i,b1.(s1/.i)) and A9: poly_with_roots(b1) = Product FlattenSeq f1 by Def11; consider f being FinSequence of (the carrier of Polynom-Ring L)*, s being FinSequence of L such that A10: len f = card support b and A11: s = canFS(support b) and A12: for i being Element of NAT st i in dom f holds f.i = fpoly_mult_root (s/.i,b.(s/.i)) and A13: poly_with_roots(b1+b2) = Product FlattenSeq f by Def11; set ff = FlattenSeq f, ff1 = FlattenSeq f1, ff2 = FlattenSeq f2; A14: len ff = degree b by A10,A11,A12,Th62; A15: len ff2 = degree b2 by A2,A3,A4,Th62; set g = (FlattenSeq f1) ^ (FlattenSeq f2); len g = len ff1 + len ff2 by FINSEQ_1:22 .= degree b1 + degree b2 by A6,A7,A8,A15,Th62 .= degree b by Th15; then A16: dom ff = dom g by A14,FINSEQ_3:29; A17: len s = card support b by A11,Th3; now let x be set; per cases; suppose x in rng ff; then consider k being Nat such that A18: k in dom ff and A19: ff.k = x by FINSEQ_2:10; consider i, j being Element of NAT such that A20: i in dom f and A21: j in dom (f.i) and k = (Sum Card (f|(i-'1))) + j and A22: (f.i).j = ff.k by A18,PRE_POLY:29; f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A12,A20; then A23: (f.i).j = <% -s/.i, 1.L %> by A21,Def10; i in dom s by A10,A17,A20,FINSEQ_3:29; then s.i = s/.i & s.i in rng s by FUNCT_1:3,PARTFUN1:def 6; then A24: s/.i in support b by A11,FUNCT_2:def 3; A25: card (g"{x}) = card (ff1"{x}) + card (ff2"{x}) by FINSEQ_3:57; per cases by A1,A24,XBOOLE_0:def 3; suppose A26: s/.i in support b1 & not s/.i in support b2; then A27: card(ff2"{x}) = 0 by A2,A3,A4,A19,A22,A23,Th63; thus card Coim(ff,x) = b.(s/.i) by A10,A11,A12,A19,A22,A23,A24,Th63 .= b1.(s/.i) + b2.(s/.i) by PRE_POLY:def 5 .= b1.(s/.i) + (0 qua Nat) by A26,PRE_POLY:def 7 .= card Coim(g,x) by A6,A7,A8,A19,A22,A23,A25,A26,A27,Th63; end; suppose A28: not s/.i in support b1 & s/.i in support b2; then A29: card(ff2"{x}) = b2.(s/.i) by A2,A3,A4,A19,A22,A23,Th63; thus card Coim(ff,x) = b.(s/.i) by A10,A11,A12,A19,A22,A23,A24,Th63 .= b1.(s/.i) + b2.(s/.i) by PRE_POLY:def 5 .= 0 qua Nat+b2.(s/.i) by A28,PRE_POLY:def 7 .= card Coim(g,x) by A6,A7,A8,A19,A22,A23,A25,A28,A29,Th63; end; suppose A30: s/.i in support b1 & s/.i in support b2; then A31: card(ff2"{x}) = b2.(s/.i) by A2,A3,A4,A19,A22,A23,Th63; thus card Coim(ff,x) = b.(s/.i) by A10,A11,A12,A19,A22,A23,A24,Th63 .= b1.(s/.i) + b2.(s/.i) by PRE_POLY:def 5 .= card Coim(g,x) by A6,A7,A8,A19,A22,A23,A25,A30,A31,Th63; end; end; suppose A32: not x in rng ff; now assume x in rng g; then A33: x in (rng ff1 \/ rng ff2) by FINSEQ_1:31; per cases by A33,XBOOLE_0:def 3; suppose x in rng ff1; then consider k being Nat such that A34: k in dom ff1 and A35: ff1.k = x by FINSEQ_2:10; consider i, j being Element of NAT such that A36: i in dom f1 and A37: j in dom (f1.i) and k = (Sum Card (f1|(i-'1))) + j and A38: (f1.i).j = ff1.k by A34,PRE_POLY:29; f1.i = fpoly_mult_root(s1/.i,b1.(s1/.i)) by A8,A36; then A39: (f1.i).j = <% -s1/.i, 1.L %> by A37,Def10; len s1 = card support b1 by A7,Th3; then i in dom s1 by A6,A36,FINSEQ_3:29; then s1.i = s1/.i & s1.i in rng s1 by FUNCT_1:3,PARTFUN1:def 6; then s1/.i in support b1 by A7,FUNCT_2:def 3; then A40: s1/.i in support b by A1,XBOOLE_0:def 3; then b.(s1/.i) <> 0 by PRE_POLY:def 7; then A41: 0 qua Nat+1 <= b.(s1/.i) by NAT_1:13; s1/.i in rng s by A11,A40,FUNCT_2:def 3; then consider l being Nat such that A42: l in dom s and A43: s.l = s1/.i by FINSEQ_2:10; A44: s.l = s/.l by A42,PARTFUN1:def 6; A45: l in dom f by A10,A17,A42,FINSEQ_3:29; then A46: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by A12; then len (f.l) = b.(s/.l) by Def10; then A47: 1 in dom (f.l) by A43,A44,A41,FINSEQ_3:25; then (Sum Card (f|(l-'1))) + 1 in dom ff & (f.l).1 = ff.((Sum Card ( f|(l-'1))) + 1) by A45,PRE_POLY:30; then (f.l).1 in rng ff by FUNCT_1:3; hence contradiction by A32,A35,A38,A39,A43,A46,A44,A47,Def10; end; suppose x in rng ff2; then consider k being Nat such that A48: k in dom ff2 and A49: ff2.k = x by FINSEQ_2:10; consider i, j being Element of NAT such that A50: i in dom f2 and A51: j in dom (f2.i) and k = (Sum Card (f2|(i-'1))) + j and A52: (f2.i).j = ff2.k by A48,PRE_POLY:29; f2.i = fpoly_mult_root(s2/.i,b2.(s2/.i)) by A4,A50; then A53: (f2.i).j = <% -s2/.i, 1.L %> by A51,Def10; len s2 = card support b2 by A3,Th3; then i in dom s2 by A2,A50,FINSEQ_3:29; then s2.i = s2/.i & s2.i in rng s2 by FUNCT_1:3,PARTFUN1:def 6; then s2/.i in support b2 by A3,FUNCT_2:def 3; then A54: s2/.i in support b by A1,XBOOLE_0:def 3; then b.(s2/.i) <> 0 by PRE_POLY:def 7; then A55: 0 qua Nat+1 <= b.(s2/.i) by NAT_1:13; s2/.i in rng s by A11,A54,FUNCT_2:def 3; then consider l being Nat such that A56: l in dom s and A57: s.l = s2/.i by FINSEQ_2:10; A58: s.l = s/.l by A56,PARTFUN1:def 6; A59: l in dom f by A10,A17,A56,FINSEQ_3:29; then A60: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by A12; then len (f.l) = b.(s/.l) by Def10; then A61: 1 in dom (f.l) by A57,A58,A55,FINSEQ_3:25; then (Sum Card (f|(l-'1))) + 1 in dom ff & (f.l).1 = ff.((Sum Card ( f|(l-'1))) + 1) by A59,PRE_POLY:30; then (f.l).1 in rng ff by FUNCT_1:3; hence contradiction by A32,A49,A52,A53,A57,A60,A58,A61,Def10; end; end; then g"{x} = {} by FUNCT_1:72; hence card Coim(ff,x) = card Coim(g,x) by A32,FUNCT_1:72; end; end; then ff, g are_fiberwise_equipotent by CLASSES1:def 9; then ex p being Permutation of dom FlattenSeq f st FlattenSeq f = (( FlattenSeq f1) ^ (FlattenSeq f2)) * p by A16,RFINSEQ:4; hence poly_with_roots(b1+b2) = Product ((FlattenSeq f1) ^ (FlattenSeq f2)) by A13 ,A16,Th16 .= (Product FlattenSeq f1) * (Product FlattenSeq f2) by GROUP_4:5 .= (poly_with_roots b1)*'(poly_with_roots b2) by A9,A5,POLYNOM3:def 10; end; theorem for L being algebraic-closed domRing, p being non-zero (Polynomial of L) st p.(len p-'1) = 1.L holds p = poly_with_roots(BRoots(p)) proof let L be algebraic-closed domRing, p be non-zero (Polynomial of L); assume A1: p.(len p-'1) = 1.L; defpred P[Nat] means for p being non-zero Polynomial of L st len p = $1 & $1 >= 1 & p.(len p -'1) = 1.L holds p = poly_with_roots(BRoots(p)); len p > 0 by Th17; then A2: len p >= 0 qua Nat+1 by NAT_1:13; A3: for n being Nat st n >= 1 & P[n] holds P[n+1] proof let n be Nat such that A4: n >= 1 and A5: P[n]; let p being non-zero Polynomial of L such that A6: len p = n+1 and n+1 >= 1 and A7: p.(len p -'1) = 1.L; n+1 > 1 by A4,NAT_1:13; then p is with_roots by A6,POLYNOM5:def 8; then consider x being Element of L such that A8: x is_a_root_of p by POLYNOM5:def 7; set r = <%-x,1.L%>; set q = poly_quotient(p,x); A9: p = r*'q by A8,Th50; then reconsider q as non-zero Polynomial of L by Th34; A10: len r = 2 by POLYNOM5:40; then A11: r.(len r -'1) <> 0.L by Th18; len q > 0 by Th17; then q.(len q -'1) <> 0.L by Th18; then r.(len r -'1) * q.(len q -'1) <> 0.L by A11,VECTSP_2:def 1; then A12: len p = len q + (1+1)- 1 by A9,A10,POLYNOM4:10; q.(len q -'1) = 1.L by A7,A9,Th41; then A13: q = poly_with_roots(BRoots(q)) by A4,A5,A6,A12; A14: poly_with_roots(({x},1)-bag) = <%-x,1.L%> by Th61; BRoots r = ({x},1)-bag by Th54; then BRoots(p) = ({x},1)-bag + BRoots(q) by A9,Th56; hence thesis by A9,A13,A14,Th64; end; A15: P[1] proof let p be non-zero Polynomial of L such that A16: len p = 1 and 1 >= 1 and A17: p.(len p -'1) = 1.L; degree BRoots p = 0 by A16,Th57; then A18: BRoots p = EmptyBag the carrier of L by Th12; len p -'1 = 0 by A16,XREAL_1:232; hence p = <%1.L%> by A16,A17,ALGSEQ_1:def 5 .= poly_with_roots(BRoots(p)) by A18,Th60; end; for n being Nat st n >= 1 holds P[n] from NAT_1:sch 8(A15,A3); hence thesis by A1,A2; end; theorem for L being comRing, s being non empty finite Subset of L, f being FinSequence of Polynom-Ring L st len f = card s & for i being Element of NAT, c being Element of L st i in dom f & c = (canFS(s)).i holds f.i = <% -c, 1.L %> holds poly_with_roots((s,1)-bag) = Product(f) proof let L be comRing; set cL = the carrier of L; set cPRL = the carrier of Polynom-Ring L; let s be non empty finite Subset of cL, f be FinSequence of cPRL such that A1: len f = card s and A2: for i being Element of NAT, c being Element of cL st i in dom f & c = (canFS(s)).i holds f.i = <% -c, 1.L %>; set cs = canFS(s); A3: rng cs = s by FUNCT_2:def 3; defpred P[Element of NAT] means ex t being finite Subset of cL, g being FinSequence of cPRL st t = rng (cs | Seg $1) & g = f | Seg $1 & poly_with_roots ((t,1)-bag) = Product(g); A4: len cs = card s by Th3; then A5: dom f = dom cs by A1,FINSEQ_3:29; A6: for j being Element of NAT st 1 <= j & j < len f holds P[j] implies P[j +1] proof let j be Element of NAT such that A7: 1 <= j and A8: j < len f; reconsider g1 = f | Seg (j+1) as FinSequence of cPRL by FINSEQ_1:18; A9: j+1 <= len f by A8,NAT_1:13; then ex l being Nat st len f = j+1+l by NAT_1:10; then A10: len g1 = j+1 by FINSEQ_3:53; 1 <= j+1 by A7,NAT_1:13; then A11: j+1 in dom cs by A1,A4,A9,FINSEQ_3:25; then cs.(j+1) in s by FINSEQ_2:11; then reconsider csj1 = cs.(j+1) as Element of cL; A12: g1.(j+1) = f.(j+1) by FINSEQ_1:4,FUNCT_1:49 .= <% -csj1, 1.L %> by A2,A5,A11; reconsider csja1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:18; reconsider csja = cs | Seg j as FinSequence of s by FINSEQ_1:18; given t being finite Subset of cL, g being FinSequence of cPRL such that A13: t = rng (cs | Seg j) and A14: g = f | Seg j and A15: poly_with_roots((t,1)-bag) = Product(g); j <= j+1 by NAT_1:12; then Seg j c= Seg (j+1) by FINSEQ_1:5; then g = g1 | Seg j by A14,RELAT_1:74; then A16: g1 = g ^ <* <% -csj1, 1.L %> *> by A10,A12,FINSEQ_3:55; reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L; set t1 = rng csja1; Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:9; then A17: csja1 = csja \/ cs|{j+1} by RELAT_1:78; cs|{j+1} = (j+1) .--> csj1 by A11,FUNCT_7:6; then rng (cs|{j+1}) = {csj1} by FUNCOP_1:8; then A18: t1 = t \/ {csj1} by A13,A17,RELAT_1:12; reconsider epj1 =<% -csj1, 1.L %> as Element of cPRL by POLYNOM3:def 10; reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L; A19: pj1 = epj1 by Th61; reconsider t1 as finite Subset of cL by A18; take t1, g1; thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1); t misses {csj1} proof assume not thesis; then t /\ {csj1} <> {} by XBOOLE_0:def 7; then consider x being set such that A20: x in t /\ {csj1} by XBOOLE_0:def 1; x in {csj1} by A20,XBOOLE_0:def 4; then A21: x = csj1 by TARSKI:def 1; x in t by A20,XBOOLE_0:def 4; then consider i being set such that A22: i in dom (cs | Seg j) and A23: x = (cs | Seg j).i by A13,FUNCT_1:def 3; A24: i in Seg j by A22,RELAT_1:57; reconsider i as Element of NAT by A22; A25: 1 <= i by A24,FINSEQ_1:1; i <= j by A24,FINSEQ_1:1; then A26: i < j+1 by NAT_1:13; x = cs.i by A22,A23,FUNCT_1:47; hence contradiction by A1,A4,A3,A9,A21,A25,A26,GRAPH_5:7; end; then (t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by A18,Th10; hence poly_with_roots((t1,1)-bag) = pt *' pj1 by Th64 .= Product(g) * epj1 by A15,A19,POLYNOM3:def 10 .= Product(g1) by A16,GROUP_4:6; end; f | Seg len f is FinSequence by FINSEQ_1:18; then A27: cs | Seg len f is FinSequence & f | Seg len f = f by FINSEQ_1:18 ,FINSEQ_2:20; A28: 0 qua Nat+1 <= len f by A1,NAT_1:13; A29: P[1] proof 1 in dom cs by A1,A4,A28,FINSEQ_3:25; then reconsider cs1 = cs.1 as Element of s by FINSEQ_2:11; reconsider g = f | Seg 1 as FinSequence of cPRL by FINSEQ_1:18; reconsider cs1a = cs | Seg 1 as FinSequence of s by FINSEQ_1:18; A30: cs1 in cL; A31: 1 in Seg 1 by FINSEQ_1:1; then A32: cs1a.1 = cs1 by FUNCT_1:49; reconsider cs1 = cs.1 as Element of cL by A30; reconsider t = {cs1} as finite Subset of cL; take t, g; consider s1 being Element of s such that A33: cs1a = <* s1 *> by A1,A4,A28,TREES_9:34; cs1a.1 = s1 by A33,FINSEQ_1:40; hence t = rng (cs | Seg 1) & g = f | Seg 1 by A33,A32,FINSEQ_1:39; consider p1 being Element of cPRL such that A34: g = <* p1 *> by A28,TREES_9:34; A35: g.1 = p1 & Product(g) = p1 by A34,FINSEQ_1:40,FINSOP_1:11; A36: 1 in dom f by A28,FINSEQ_3:25; then reconsider f1 = f.1 as Element of cPRL by FINSEQ_2:11; A37: g.1 = f1 by A31,FUNCT_1:49; f1 = <% -cs1, 1.L %> by A2,A36; hence thesis by A37,A35,Th61; end; for i being Element of NAT st 1 <= i & i <= len f holds P[i] from INT_1:sch 7 (A29,A6); then ex t being finite Subset of cL, g being FinSequence of cPRL st t = rng ( cs | Seg len f) & g = f | Seg len f & poly_with_roots((t,1)-bag ) = Product(g) by A28; hence thesis by A1,A4,A27,A3,FINSEQ_2:20; end; theorem for L being non trivial comRing, s being non empty finite Subset of L, x being Element of L, f being FinSequence of L st len f = card s & for i being Element of NAT, c being Element of L st i in dom f & c = (canFS(s)).i holds f.i = eval(<% -c, 1.L %>,x) holds eval(poly_with_roots((s,1)-bag),x) = Product(f) proof let L be non trivial comRing; set cL = the carrier of L; let s be non empty finite Subset of cL, x be Element of cL, f be FinSequence of L such that A1: len f = card s and A2: for i being Element of NAT, c being Element of cL st i in dom f & c = (canFS(s)).i holds f.i = eval(<% -c, 1.L %>,x); set cs = canFS(s); A3: rng cs = s by FUNCT_2:def 3; defpred P[Element of NAT] means ex t being finite Subset of cL, g being FinSequence of cL st t = rng (cs | Seg $1) & g = f | Seg $1 & eval( poly_with_roots((t,1)-bag),x) = Product(g); A4: len cs = card s by Th3; then A5: dom f = dom cs by A1,FINSEQ_3:29; A6: for j being Element of NAT st 1 <= j & j < len f holds P[j] implies P[j +1] proof let j be Element of NAT such that A7: 1 <= j and A8: j < len f; reconsider g1 = f | Seg (j+1) as FinSequence of cL by FINSEQ_1:18; A9: j+1 <= len f by A8,NAT_1:13; then ex l being Nat st len f = j+1+l by NAT_1:10; then A10: len g1 = j+1 by FINSEQ_3:53; 1 <= j+1 by A7,NAT_1:13; then A11: j+1 in dom cs by A1,A4,A9,FINSEQ_3:25; then cs.(j+1) in s by FINSEQ_2:11; then reconsider csj1 = cs.(j+1) as Element of cL; A12: g1.(j+1) = f.(j+1) by FINSEQ_1:4,FUNCT_1:49 .= eval(<% -csj1, 1.L %>,x) by A2,A5,A11; reconsider csja1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:18; reconsider csja = cs | Seg j as FinSequence of s by FINSEQ_1:18; given t being finite Subset of cL, g being FinSequence of cL such that A13: t = rng (cs | Seg j) and A14: g = f | Seg j and A15: eval(poly_with_roots((t,1)-bag),x) = Product(g); j <= j+1 by NAT_1:12; then Seg j c= Seg (j+1) by FINSEQ_1:5; then g = g1 | Seg j by A14,RELAT_1:74; then A16: g1 = g ^ <* eval(<% -csj1, 1.L %>,x) *> by A10,A12,FINSEQ_3:55; reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L; set t1 = rng csja1; Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:9; then A17: csja1 = csja \/ cs|{j+1} by RELAT_1:78; cs|{j+1} = (j+1) .--> csj1 by A11,FUNCT_7:6; then rng (cs|{j+1}) = {csj1} by FUNCOP_1:8; then A18: t1 = t \/ {csj1} by A13,A17,RELAT_1:12; then reconsider t1 as finite Subset of cL; take t1, g1; thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1); reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L; A19: pj1 = <% -csj1, 1.L %> by Th61; t misses {csj1} proof assume not thesis; then t /\ {csj1} <> {} by XBOOLE_0:def 7; then consider x being set such that A20: x in t /\ {csj1} by XBOOLE_0:def 1; x in {csj1} by A20,XBOOLE_0:def 4; then A21: x = csj1 by TARSKI:def 1; x in t by A20,XBOOLE_0:def 4; then consider i being set such that A22: i in dom (cs | Seg j) and A23: x = (cs | Seg j).i by A13,FUNCT_1:def 3; A24: i in Seg j by A22,RELAT_1:57; reconsider i as Element of NAT by A22; A25: 1 <= i by A24,FINSEQ_1:1; i <= j by A24,FINSEQ_1:1; then A26: i < j+1 by NAT_1:13; x = cs.i by A22,A23,FUNCT_1:47; hence contradiction by A1,A4,A3,A9,A21,A25,A26,GRAPH_5:7; end; then (t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by A18,Th10; then poly_with_roots((t1,1)-bag) = pt *' pj1 by Th64; hence eval(poly_with_roots((t1,1)-bag),x) = Product(g) * eval(pj1,x) by A15, POLYNOM4:24 .= Product(g1) by A16,A19,GROUP_4:6; end; f | Seg len f is FinSequence by FINSEQ_1:18; then A27: cs | Seg len f is FinSequence & f | Seg len f = f by FINSEQ_1:18 ,FINSEQ_2:20; A28: 0 qua Nat+1 <= len f by A1,NAT_1:13; A29: P[1] proof 1 in dom cs by A1,A4,A28,FINSEQ_3:25; then reconsider cs1 = cs.1 as Element of s by FINSEQ_2:11; reconsider g = f | Seg 1 as FinSequence of cL by FINSEQ_1:18; reconsider cs1a = cs | Seg 1 as FinSequence of s by FINSEQ_1:18; A30: cs1 in cL; A31: 1 in Seg 1 by FINSEQ_1:1; then A32: cs1a.1 = cs1 by FUNCT_1:49; reconsider cs1 = cs.1 as Element of cL by A30; reconsider t = {cs1} as finite Subset of cL; take t, g; consider s1 being Element of s such that A33: cs1a = <* s1 *> by A1,A4,A28,TREES_9:34; cs1a.1 = s1 by A33,FINSEQ_1:40; hence t = rng (cs | Seg 1) & g = f | Seg 1 by A33,A32,FINSEQ_1:39; consider p1 being Element of cL such that A34: g = <* p1 *> by A28,TREES_9:34; A35: g.1 = p1 & Product(g) = p1 by A34,FINSEQ_1:40,FINSOP_1:11; A36: 1 in dom f by A28,FINSEQ_3:25; then reconsider f1 = f.1 as Element of cL by FINSEQ_2:11; A37: g.1 = f1 by A31,FUNCT_1:49; f1 = eval(<% -cs1, 1.L %>,x) by A2,A36; hence thesis by A37,A35,Th61; end; for i being Element of NAT st 1 <= i & i <= len f holds P[i] from INT_1:sch 7 (A29,A6); then ex t being finite Subset of cL, g being FinSequence of cL st t = rng (cs | Seg len f) & g = f | Seg len f & eval(poly_with_roots((t,1 )-bag),x) = Product(g) by A28; hence thesis by A1,A4,A27,A3,FINSEQ_2:20; end;