:: UPROOTS semantic presentation begin theorem Th1: :: UPROOTS:1 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 S1[ 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 ; ::_thesis: ( ( for i being Element of NAT st i in dom f holds f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) ) A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] let f be FinSequence of NAT ; ::_thesis: ( len f = n + 1 & ( for i being Element of NAT st i in dom f holds f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) ) assume that A3: len f = n + 1 and A4: for i being Element of NAT st i in dom f holds f . i <> 0 ; ::_thesis: ( Sum f = len f iff f = (len f) |-> 1 ) consider g being FinSequence of NAT , a being Element of NAT such that A5: f = g ^ <*a*> by A3, FINSEQ_2:19; A6: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g_holds_ g_._i_<>_0 let i be Element of NAT ; ::_thesis: ( i in dom g implies g . i <> 0 ) A7: dom g c= dom f by A5, FINSEQ_1:26; assume A8: i in dom g ; ::_thesis: g . i <> 0 then f . i = g . i by A5, FINSEQ_1:def_7; hence g . i <> 0 by A4, A8, A7; ::_thesis: verum 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, FINSEQ_1:def_3; then a <> 0 by A3, A4, FINSEQ_1:4; then A10: 0 + 1 <= a by NAT_1:13; A11: g is FinSequence of REAL by FINSEQ_2:24; hereby ::_thesis: ( f = (len f) |-> 1 implies Sum f = len f ) reconsider h = (len g) |-> 1 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 ; ::_thesis: f = (len f) |-> 1 A13: Sum g = ((Sum g) + a) - a .= (n + 1) - a by A3, A5, A12, RVSUM_1:74 ; A14: now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(len_g)_holds_ h1_._j_<=_g1_._j let j be Nat; ::_thesis: ( j in Seg (len g) implies h1 . j <= g1 . j ) reconsider a = j as Element of NAT by ORDINAL1:def_12; assume A15: j in Seg (len g) ; ::_thesis: h1 . j <= g1 . j then j in dom g by FINSEQ_1:def_3; then g . j <> 0 by A6; then 0 + 1 <= g . a by NAT_1:13; hence h1 . j <= g1 . j by A15, FUNCOP_1:7; ::_thesis: verum 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; ::_thesis: verum end; assume f = (len f) |-> 1 ; ::_thesis: Sum f = len f 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 Sum f = len f by A2, A3, A9, A6, A20, A19; ::_thesis: verum end; A21: S1[ 0 ] proof let f be FinSequence of NAT ; ::_thesis: ( len f = 0 & ( for i being Element of NAT st i in dom f holds f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) ) assume that A22: len f = 0 and for i being Element of NAT st i in dom f holds f . i <> 0 ; ::_thesis: ( Sum f = len f iff f = (len f) |-> 1 ) hereby ::_thesis: ( f = (len f) |-> 1 implies Sum f = len f ) assume Sum f = len f ; ::_thesis: f = (len f) |-> 1 thus f = {} by A22 .= (len f) |-> 1 by A22 ; ::_thesis: verum end; assume f = (len f) |-> 1 ; ::_thesis: Sum f = len f f = {} by A22; hence Sum f = len f by RVSUM_1:72; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A1); hence ( ( for i being Element of NAT st i in dom f holds f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) ) ; ::_thesis: verum end; scheme :: UPROOTS:sch 1 IndFinSeq0{ F1() -> Nat, P1[ set ] } : for i being Element of NAT st 1 <= i & i <= F1() holds P1[i] provided A1: P1[1] and A2: for i being Element of NAT st 1 <= i & i < F1() & P1[i] holds P1[i + 1] proof defpred S1[ Nat] means ( 1 <= $1 & $1 <= F1() & P1[$1] ); assume ex i being Element of NAT st ( 1 <= i & i <= F1() & P1[i] ) ; ::_thesis: contradiction then A3: ex k being Nat st S1[k] ; consider k being Nat such that A4: ( S1[k] & ( for k9 being Nat st S1[k9] holds k <= k9 ) ) from NAT_1:sch_5(A3); percases ( k = 1 or k <> 1 ) ; suppose k = 1 ; ::_thesis: contradiction hence contradiction by A1, A4; ::_thesis: verum end; supposeA5: k <> 1 ; ::_thesis: contradiction 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 ; 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 < F1() by A4, XXREAL_0:2; hence contradiction by A2, A4, A6, A8, A7; ::_thesis: verum end; end; end; theorem Th2: :: UPROOTS:2 for L being non empty right_complementable add-associative right_zeroed addLoopStr for r being 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 non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for r being 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) let r be FinSequence of L; ::_thesis: ( len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds r . k = 0. L ) implies Sum r = (r /. 1) + (r /. 2) ) assume 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 ; ::_thesis: Sum r = (r /. 1) + (r /. 2) 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; not r is 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__::_thesis:_not_r1_is_empty assume r1 is empty ; ::_thesis: contradiction then len r1 = 0 ; hence contradiction by A1, A9; ::_thesis: verum 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__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_r2_holds_ r2_._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom r2 implies r2 . i = 0. L ) assume A14: i in dom r2 ; ::_thesis: r2 . i = 0. L 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 ; ::_thesis: verum 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 ; ::_thesis: verum end; begin registration let A be finite set ; cluster Relation-like NAT -defined A -valued Function-like one-to-one onto finite FinSequence-like FinSubsequence-like finite-support for FinSequence of A; existence ex b1 being FinSequence of A st ( b1 is one-to-one & b1 is onto ) proof defpred S1[ Element of NAT , set , set ] means c3 = [(choose (c2 `2)),((c2 `2) \ {(choose (c2 `2))})]; set cA = card A; A1: for n being Element of NAT st 1 <= n & n < card A holds for x being set ex y being set st S1[n,x,y] ; consider f being FinSequence such that A2: len f = card A and A3: ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) and A4: for n being Element of NAT st 1 <= n & n < card A holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_3(A1); defpred S2[ Element of NAT ] means ( A in dom f implies ( f . A in [:A,(bool A):] & ex X being finite set st ( X = (f . A) `2 & (card X) + A = card A ) ) ); A5: for i being Element of NAT st 1 <= i & i < len f & S2[i] holds S2[i + 1] proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] ) assume that A6: 1 <= i and A7: i < len f and A8: S2[i] and i + 1 in dom f ; ::_thesis: ( f . (i + 1) in [:A,(bool A):] & ex X being finite set st ( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A ) ) A9: f . (i + 1) = [(choose ((f . i) `2)),(((f . i) `2) \ {(choose ((f . i) `2))})] by A2, A4, A6, A7; consider a, ba being set such that a in A and A10: ba in bool A and A11: f . i = [a,ba] by A6, A7, A8, FINSEQ_3:25, ZFMISC_1:def_2; A12: (f . i) `2 = ba by A11, MCART_1:7; then A13: ((f . i) `2) \ {(choose ((f . i) `2))} c= A by A10, XBOOLE_1:1; A14: now__::_thesis:_not_choose_((f_._i)_`2)_in_((f_._i)_`2)_\_{(choose_((f_._i)_`2))} assume choose ((f . i) `2) in ((f . i) `2) \ {(choose ((f . i) `2))} ; ::_thesis: contradiction then not choose ((f . i) `2) in {(choose ((f . i) `2))} by XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; consider X being finite set such that A15: X = (f . i) `2 and A16: (card X) + i = card A by A6, A7, A8, FINSEQ_3:25; A17: X <> {} 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; ::_thesis: ex X being finite set st ( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A ) reconsider XX = ((f . i) `2) \ {(choose ((f . i) `2))} as finite set by A15; take XX ; ::_thesis: ( XX = (f . (i + 1)) `2 & (card XX) + (i + 1) = card A ) thus XX = (f . (i + 1)) `2 by A9, MCART_1:7; ::_thesis: (card XX) + (i + 1) = card A {(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 (card XX) + (i + 1) = card A by A16; ::_thesis: verum end; A18: S2[1] proof reconsider X = A \ {(choose A)} as finite set ; A19: now__::_thesis:_not_choose_A_in_A_\_{(choose_A)} assume choose A in A \ {(choose A)} ; ::_thesis: contradiction then not choose A in {(choose A)} by XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; assume A20: 1 in dom f ; ::_thesis: ( f . 1 in [:A,(bool A):] & ex X being finite set st ( X = (f . 1) `2 & (card X) + 1 = card A ) ) then A <> {} by A2, FINSEQ_3:25; hence f . 1 in [:A,(bool A):] by A3, ZFMISC_1:def_2; ::_thesis: ex X being finite set st ( X = (f . 1) `2 & (card X) + 1 = card A ) take X ; ::_thesis: ( X = (f . 1) `2 & (card X) + 1 = card A ) thus X = (f . 1) `2 by A2, A3, A20, FINSEQ_3:25, MCART_1:7; ::_thesis: (card X) + 1 = card A 0 + 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 (card X) + 1 = card A by A19, CARD_2:41; ::_thesis: verum end; A21: for i being Element of NAT st 1 <= i & i <= len f holds S2[i] from UPROOTS:sch_1(A18, A5); rng f c= [:A,(bool A):] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [:A,(bool A):] ) assume y in rng f ; ::_thesis: y in [:A,(bool A):] 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 y in [:A,(bool A):] by A21, A22, A23; ::_thesis: verum end; then reconsider f = f as FinSequence of [:A,(bool A):] by FINSEQ_1:def_4; deffunc H1( Nat) -> set = (f . A) `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 = H1(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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in A ) assume y in rng p ; ::_thesis: y in A 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 y in A by A28, MCART_1:10; ::_thesis: verum end; then reconsider p = p as FinSequence of A by FINSEQ_1:def_4; A29: rng p = A proof set F = p; percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: rng p = A hence rng p = A ; ::_thesis: verum end; supposeA30: A <> {} ; ::_thesis: rng p = A defpred S3[ Element of NAT ] means ( (rng (p | (Seg A))) \/ ((f . A) `2) = A & ex X being finite set st ( X = (f . A) `2 & (card X) + A = card A ) ); A31: for i being Element of NAT st 1 <= i & i < len f & S3[i] holds S3[i + 1] proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f & S3[i] implies S3[i + 1] ) assume that A32: 1 <= i and A33: i < len f and A34: S3[i] ; ::_thesis: S3[i + 1] 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 = card A by A34; reconsider XX = ((f . i) `2) \ {(choose ((f . i) `2))} as finite set by A36; not (f . i) `2 is 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 = p | (Seg i), Fi1 = p | (Seg (i + 1)) as FinSequence of A by FINSEQ_1:18; A39: i + 1 <= len p 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 p by A39, FINSEQ_3:25; A42: rng Fi1 = (rng Fi) \/ (rng <*a*>) by A40, FINSEQ_1:31 .= (rng Fi) \/ {a} by FINSEQ_1:39 ; ( p . (i + 1) = Fi1 . (i + 1) & i = len Fi ) by A2, A24, A33, FINSEQ_1:4, FINSEQ_1:17, FUNCT_1:49; then A43: a = p . (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 (p | (Seg (i + 1)))) \/ ((f . (i + 1)) `2) = A by A34, A38, A42, A43, XBOOLE_1:4; ::_thesis: ex X being finite set st ( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A ) take XX ; ::_thesis: ( XX = (f . (i + 1)) `2 & (card XX) + (i + 1) = card A ) thus XX = (f . (i + 1)) `2 by A35, MCART_1:7; ::_thesis: (card XX) + (i + 1) = card A now__::_thesis:_not_choose_((f_._i)_`2)_in_((f_._i)_`2)_\_{(choose_((f_._i)_`2))} assume choose ((f . i) `2) in ((f . i) `2) \ {(choose ((f . i) `2))} ; ::_thesis: contradiction then not choose ((f . i) `2) in {(choose ((f . i) `2))} by XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then card X = (card XX) + 1 by A36, A38, CARD_2:41; hence (card XX) + (i + 1) = card A by A37; ::_thesis: verum end; A44: 0 + 1 <= len p by A24, A30, NAT_1:13; then A45: 1 in dom p by FINSEQ_3:25; A46: S3[1] proof reconsider X = A \ {(choose A)} as finite set ; reconsider F1 = p | (Seg 1) as FinSequence of A by FINSEQ_1:18; A47: now__::_thesis:_not_choose_A_in_A_\_{(choose_A)} assume choose A in A \ {(choose A)} ; ::_thesis: contradiction then not choose A in {(choose A)} by XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; 1 in Seg (0 + 1) by FINSEQ_1:4; then A48: F1 . 1 = p . 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 p | (Seg 1) = <*(choose A)*> by A48, FINSEQ_1:40; then A49: rng (p | (Seg 1)) = {(choose A)} by FINSEQ_1:39; (f . 1) `2 = A \ {(choose A)} by A3, A30, MCART_1:7; hence (rng (p | (Seg 1))) \/ ((f . 1) `2) = A by A49, XBOOLE_1:45; ::_thesis: ex X being finite set st ( X = (f . 1) `2 & (card X) + 1 = card A ) take X ; ::_thesis: ( X = (f . 1) `2 & (card X) + 1 = card A ) thus X = (f . 1) `2 by A3, A30, MCART_1:7; ::_thesis: (card X) + 1 = card A {(choose A)} c= A by A30, ZFMISC_1:31; then A = {(choose A)} \/ (A \ {(choose A)}) by XBOOLE_1:45; hence (card X) + 1 = card A by A47, CARD_2:41; ::_thesis: verum end; A50: for i being Element of NAT st 1 <= i & i <= len f holds S3[i] from UPROOTS:sch_1(A46, A31); A51: len p >= 1 by A24, A30, NAT_1:14; then consider X being finite set such that A52: X = (f . (len p)) `2 and A53: (card X) + (len f) = card A by A2, A24, A50; p = p | (Seg (len p)) by FINSEQ_3:49; then A54: (rng p) \/ ((f . (len p)) `2) = A by A2, A24, A50, A51; X = {} by A2, A53; hence rng p = A by A54, A52; ::_thesis: verum end; end; end; then A55: p is onto by FUNCT_2:def_3; take p ; ::_thesis: ( p is one-to-one & p is onto ) p is one-to-one by A24, A29, FINSEQ_4:62; hence ( p is one-to-one & p is onto ) by A55; ::_thesis: verum end; end; definition let A be finite set ; func canFS A -> FinSequence of A equals :: UPROOTS:def 1 the one-to-one onto FinSequence of A; coherence the one-to-one onto FinSequence of A is FinSequence of A ; end; :: deftheorem defines canFS UPROOTS:def_1_:_ for A being finite set holds canFS A = the one-to-one onto FinSequence of A; registration let A be finite set ; cluster canFS A -> one-to-one onto ; coherence ( canFS A is one-to-one & canFS A is onto ) ; end; theorem Th3: :: UPROOTS:3 for A being finite set holds len (canFS A) = card A proof let A be finite set ; ::_thesis: len (canFS A) = card A rng (canFS A) = A by FUNCT_2:def_3; hence len (canFS A) = card A by FINSEQ_4:62; ::_thesis: verum end; registration let A be non empty finite set ; cluster canFS A -> non empty ; coherence not canFS A is empty proof len (canFS A) = card A by Th3; hence not canFS A is empty ; ::_thesis: verum end; end; theorem Th4: :: UPROOTS:4 for a being set holds canFS {a} = <*a*> proof let a be set ; ::_thesis: canFS {a} = <*a*> A1: rng (canFS {a}) = {a} by FUNCT_2:def_3; len (canFS {a}) = card {a} by Th3 .= 1 by CARD_1:30 ; hence canFS {a} = <*a*> by A1, FINSEQ_1:39; ::_thesis: verum end; theorem Th5: :: UPROOTS:5 for A being finite set holds (canFS A) " is Function of A,(Seg (card A)) proof let A be finite set ; ::_thesis: (canFS A) " is Function of A,(Seg (card A)) 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 (canFS A) " is Function of A,(Seg (card A)) by A1, FUNCT_2:1; ::_thesis: verum end; begin definition let X be set ; let S be finite Subset of X; let n be Element of NAT ; func(S,n) -bag -> Element of Bags X equals :: UPROOTS:def 2 (EmptyBag X) +* (S --> n); correctness coherence (EmptyBag X) +* (S --> n) is Element of Bags X; 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__::_thesis:_for_i_being_set_st_not_i_in_S_holds_ ((EmptyBag_X)_+*_(S_-->_n))_._i_=_0 let i be set ; ::_thesis: ( not i in S implies ((EmptyBag X) +* (S --> n)) . i = 0 ) assume not i in S ; ::_thesis: ((EmptyBag X) +* (S --> n)) . i = 0 hence ((EmptyBag X) +* (S --> n)) . i = (EmptyBag X) . i by A2, FUNCT_4:11 .= 0 by PRE_POLY:52 ; ::_thesis: verum end; A4: now__::_thesis:_for_i_being_set_st_i_in_S_holds_ ((EmptyBag_X)_+*_(S_-->_n))_._i_=_n let i be set ; ::_thesis: ( i in S implies ((EmptyBag X) +* (S --> n)) . i = n ) assume A5: i in S ; ::_thesis: ((EmptyBag X) +* (S --> n)) . i = n thus ((EmptyBag X) +* (S --> n)) . i = (S --> n) . i by A2, A5, FUNCT_4:13 .= n by A5, FUNCOP_1:7 ; ::_thesis: verum end; A6: support ((EmptyBag X) +* (S --> n)) is finite proof percases ( S is empty or ( not S is empty & n = 0 ) or ( not S is empty & n <> 0 ) ) ; supposeA7: S is empty ; ::_thesis: support ((EmptyBag X) +* (S --> n)) is finite now__::_thesis:_support_((EmptyBag_X)_+*_(S_-->_n))_is_empty assume not support ((EmptyBag X) +* (S --> n)) is empty ; ::_thesis: contradiction then consider x being set such that A8: x in support ((EmptyBag X) +* (S --> n)) by XBOOLE_0:def_1; ((EmptyBag X) +* (S --> n)) . x <> 0 by A8, PRE_POLY:def_7; hence contradiction by A3, A7; ::_thesis: verum end; hence support ((EmptyBag X) +* (S --> n)) is finite ; ::_thesis: verum end; supposeA9: ( not S is empty & n = 0 ) ; ::_thesis: support ((EmptyBag X) +* (S --> n)) is finite now__::_thesis:_support_((EmptyBag_X)_+*_(S_-->_n))_is_empty assume not support ((EmptyBag X) +* (S --> n)) is empty ; ::_thesis: contradiction then consider x being set such that A10: x in support ((EmptyBag X) +* (S --> n)) by XBOOLE_0:def_1; A11: ((EmptyBag X) +* (S --> n)) . x <> 0 by A10, PRE_POLY:def_7; then ((EmptyBag X) +* (S --> n)) . 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; ::_thesis: verum end; hence support ((EmptyBag X) +* (S --> n)) is finite ; ::_thesis: verum end; suppose ( not S is empty & n <> 0 ) ; ::_thesis: support ((EmptyBag X) +* (S --> n)) is finite then for x being set holds ( x in S iff ((EmptyBag X) +* (S --> n)) . x <> 0 ) by A3, A4; hence support ((EmptyBag X) +* (S --> n)) is finite by PRE_POLY:def_7; ::_thesis: verum end; end; end; dom ((EmptyBag X) +* (S --> n)) = (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 (EmptyBag X) +* (S --> n) is Element of Bags X by PRE_POLY:def_12; ::_thesis: verum end; end; :: deftheorem defines -bag UPROOTS:def_2_:_ for X being set for S being finite Subset of X for n being Element of NAT holds (S,n) -bag = (EmptyBag X) +* (S --> n); theorem Th6: :: UPROOTS:6 for X being set for S being finite Subset of X for n being Element of NAT for i being set st not i in S holds ((S,n) -bag) . i = 0 proof let X be set ; ::_thesis: for S being finite Subset of X for n being Element of NAT for i being set st not i in S holds ((S,n) -bag) . i = 0 let S be finite Subset of X; ::_thesis: for n being Element of NAT for i being set st not i in S holds ((S,n) -bag) . i = 0 let n be Element of NAT ; ::_thesis: for i being set st not i in S holds ((S,n) -bag) . i = 0 let i be set ; ::_thesis: ( not i in S implies ((S,n) -bag) . i = 0 ) assume A1: not i in S ; ::_thesis: ((S,n) -bag) . i = 0 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 ; ::_thesis: verum end; theorem Th7: :: UPROOTS:7 for X being set for S being finite Subset of X for n being Element of NAT for i being set st i in S holds ((S,n) -bag) . i = n proof let X be set ; ::_thesis: for S being finite Subset of X for n being Element of NAT for i being set st i in S holds ((S,n) -bag) . i = n let S be finite Subset of X; ::_thesis: for n being Element of NAT for i being set st i in S holds ((S,n) -bag) . i = n let n be Element of NAT ; ::_thesis: for i being set st i in S holds ((S,n) -bag) . i = n let i be set ; ::_thesis: ( i in S implies ((S,n) -bag) . i = n ) assume A1: i in S ; ::_thesis: ((S,n) -bag) . i = n 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 ; ::_thesis: verum end; theorem Th8: :: UPROOTS:8 for X being set for S being finite Subset of X for n being Element of NAT st n <> 0 holds support ((S,n) -bag) = S proof let X be set ; ::_thesis: for S being finite Subset of X for n being Element of NAT st n <> 0 holds support ((S,n) -bag) = S let S be finite Subset of X; ::_thesis: for n being Element of NAT st n <> 0 holds support ((S,n) -bag) = S let n be Element of NAT ; ::_thesis: ( n <> 0 implies support ((S,n) -bag) = S ) assume n <> 0 ; ::_thesis: support ((S,n) -bag) = S then for x being set holds ( x in S iff ((S,n) -bag) . x <> 0 ) by Th6, Th7; hence support ((S,n) -bag) = S by PRE_POLY:def_7; ::_thesis: verum end; theorem :: UPROOTS:9 for X being set for S being finite Subset of X for n being Element of NAT st ( S is empty or n = 0 ) holds (S,n) -bag = EmptyBag X proof let X be set ; ::_thesis: for S being finite Subset of X for n being Element of NAT st ( S is empty or n = 0 ) holds (S,n) -bag = EmptyBag X let S be finite Subset of X; ::_thesis: for n being Element of NAT st ( S is empty or n = 0 ) holds (S,n) -bag = EmptyBag X let n be Element of NAT ; ::_thesis: ( ( S is empty or n = 0 ) implies (S,n) -bag = EmptyBag X ) assume A1: ( S is empty or n = 0 ) ; ::_thesis: (S,n) -bag = EmptyBag X now__::_thesis:_for_i_being_set_st_i_in_X_holds_ ((S,n)_-bag)_._i_=_(EmptyBag_X)_._i let i be set ; ::_thesis: ( i in X implies ((S,n) -bag) . b1 = (EmptyBag X) . b1 ) assume i in X ; ::_thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1 percases ( i in S or not i in S ) ; suppose i in S ; ::_thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1 hence ((S,n) -bag) . i = 0 by A1, Th7 .= (EmptyBag X) . i by PRE_POLY:52 ; ::_thesis: verum end; suppose not i in S ; ::_thesis: ((S,n) -bag) . b1 = (EmptyBag X) . b1 hence ((S,n) -bag) . i = 0 by Th6 .= (EmptyBag X) . i by PRE_POLY:52 ; ::_thesis: verum end; end; end; hence (S,n) -bag = EmptyBag X by PBOOLE:3; ::_thesis: verum end; theorem Th10: :: UPROOTS:10 for X being set for S, T being finite Subset of X for 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 ; ::_thesis: for S, T being finite Subset of X for n being Element of NAT st S misses T holds ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) let S, T be finite Subset of X; ::_thesis: for n being Element of NAT st S misses T holds ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) let n be Element of NAT ; ::_thesis: ( S misses T implies ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) ) assume S misses T ; ::_thesis: ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) then A1: S /\ T = {} by XBOOLE_0:def_7; now__::_thesis:_for_i_being_set_st_i_in_X_holds_ (((S_\/_T),n)_-bag)_._i_=_(((S,n)_-bag)_+_((T,n)_-bag))_._i let i be set ; ::_thesis: ( i in X implies (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1 ) assume i in X ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1 percases ( not i in S \/ T or i in S or i in T ) by XBOOLE_0:def_3; supposeA2: not i in S \/ T ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1 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 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 ; ::_thesis: verum end; supposeA5: i in S ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1 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 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 ; ::_thesis: verum end; supposeA7: i in T ; ::_thesis: (((S \/ T),n) -bag) . b1 = (((S,n) -bag) + ((T,n) -bag)) . b1 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 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 ; ::_thesis: verum end; end; end; hence ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) by PBOOLE:3; ::_thesis: verum end; definition let X be set ; mode Rbag of X is real-valued finite-support ManySortedSet of X; end; definition let A be set ; let b be Rbag of A; func Sum b -> real number means :Def3: :: UPROOTS:def 3 ex f being FinSequence of REAL st ( it = Sum f & f = b * (canFS (support b)) ); existence ex b1 being real number ex f being FinSequence of REAL st ( b1 = Sum f & f = b * (canFS (support b)) ) proof set cS = canFS (support b); set f = b * (canFS (support b)); A1: rng (b * (canFS (support b))) c= REAL ; ( support b c= dom b & rng (canFS (support b)) = support b ) by FUNCT_2:def_3, PRE_POLY:37; then dom (b * (canFS (support b))) = dom (canFS (support b)) by RELAT_1:27; then dom (b * (canFS (support b))) = Seg (len (canFS (support b))) by FINSEQ_1:def_3; then b * (canFS (support b)) is FinSequence by FINSEQ_1:def_2; then reconsider f = b * (canFS (support b)) as FinSequence of REAL by A1, FINSEQ_1:def_4; take Sum f ; ::_thesis: ex f being FinSequence of REAL st ( Sum f = Sum f & f = b * (canFS (support b)) ) thus ex f being FinSequence of REAL st ( Sum f = Sum f & f = b * (canFS (support b)) ) ; ::_thesis: verum end; uniqueness for b1, b2 being real number st ex f being FinSequence of REAL st ( b1 = Sum f & f = b * (canFS (support b)) ) & ex f being FinSequence of REAL st ( b2 = Sum f & f = b * (canFS (support b)) ) holds b1 = b2 ; end; :: deftheorem Def3 defines Sum UPROOTS:def_3_:_ for A being set for b being Rbag of A for b3 being real number holds ( b3 = Sum b iff ex f being FinSequence of REAL st ( b3 = Sum f & f = b * (canFS (support b)) ) ); notation let A be set ; let b be bag of A; synonym degree b for Sum b; end; definition let A be set ; let b be bag of A; :: original: Sum redefine func degree b -> Element of NAT means :Def4: :: UPROOTS:def 4 ex f being FinSequence of NAT st ( it = Sum f & f = b * (canFS (support b)) ); coherence Sum b is Element of NAT 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT ) assume y in rng f ; ::_thesis: y in NAT 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 y in NAT by A4; ::_thesis: verum end; then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4; Sum f is Element of NAT ; hence Sum b is Element of NAT by A1; ::_thesis: verum end; compatibility for b1 being Element of NAT holds ( b1 = Sum b iff ex f being FinSequence of NAT st ( b1 = Sum f & f = b * (canFS (support b)) ) ) proof set cS = canFS (support b); let n be Element of NAT ; ::_thesis: ( n = Sum b iff ex f being FinSequence of NAT st ( n = Sum f & f = b * (canFS (support b)) ) ) hereby ::_thesis: ( ex f being FinSequence of NAT st ( n = Sum f & f = b * (canFS (support b)) ) implies n = Sum b ) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT ) assume y in rng f ; ::_thesis: y in NAT 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 y in NAT by A9; ::_thesis: verum end; assume A10: n = degree b ; ::_thesis: ex f being FinSequence of NAT st ( n = Sum f & f = b * (canFS (support b)) ) reconsider f = f as FinSequence of NAT by A7, FINSEQ_1:def_4; take f = f; ::_thesis: ( n = Sum f & f = b * (canFS (support b)) ) thus ( n = Sum f & f = b * (canFS (support b)) ) by A10, A5, A6; ::_thesis: verum end; given f being FinSequence of NAT such that A11: ( n = Sum f & f = b * (canFS (support b)) ) ; ::_thesis: n = Sum b rng f c= REAL ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; f = f ; hence n = Sum b by A11, Def3; ::_thesis: verum end; end; :: deftheorem Def4 defines degree UPROOTS:def_4_:_ for A being set for b being bag of A for b3 being Element of NAT holds ( b3 = degree b iff ex f being FinSequence of NAT st ( b3 = Sum f & f = b * (canFS (support b)) ) ); theorem Th11: :: UPROOTS:11 for A being set for b being Rbag of A st b = EmptyBag A holds Sum b = 0 proof let A be set ; ::_thesis: for b being Rbag of A st b = EmptyBag A holds Sum b = 0 let b be Rbag of A; ::_thesis: ( b = EmptyBag A implies Sum b = 0 ) set cS = canFS (support b); assume b = EmptyBag A ; ::_thesis: Sum b = 0 then support b = {} by BAGORDER:18; then b * (canFS (support b)) = <*> NAT ; hence Sum b = 0 by Def3, RVSUM_1:72; ::_thesis: verum end; theorem Th12: :: UPROOTS:12 for A being set for b being bag of A st Sum b = 0 holds b = EmptyBag A proof let A be set ; ::_thesis: for b being bag of A st Sum b = 0 holds b = EmptyBag A let b be bag of A; ::_thesis: ( Sum b = 0 implies b = EmptyBag 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 ; ::_thesis: b = EmptyBag A now__::_thesis:_not_support_b_<>_{} assume A4: support b <> {} ; ::_thesis: contradiction A5: now__::_thesis:_ex_i_being_Nat_st_ (_i_in_dom_f_&_0_<_f_._i_) consider x being set such that A6: x in support b by A4, XBOOLE_0:def_1; x in rng (canFS (support b)) by A6, FUNCT_2:def_3; then consider i being Nat such that A7: i in dom (canFS (support b)) and A8: (canFS (support b)) . i = x by FINSEQ_2:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; f . i = b . ((canFS (support b)) . 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; ::_thesis: verum end; for i being Nat st i in dom f holds 0 <= f . i ; hence contradiction by A3, A1, A5, RVSUM_1:85; ::_thesis: verum end; hence b = EmptyBag A by BAGORDER:19; ::_thesis: verum end; theorem Th13: :: UPROOTS:13 for A being set for S being finite Subset of A for b being bag of A holds ( ( S = support b & degree b = card S ) iff b = (S,1) -bag ) proof let A be set ; ::_thesis: for S being finite Subset of A for b being bag of A holds ( ( S = support b & degree b = card S ) iff b = (S,1) -bag ) let S be finite Subset of A; ::_thesis: for b being bag of A holds ( ( S = support b & degree b = card S ) iff b = (S,1) -bag ) let b be bag of A; ::_thesis: ( ( S = support b & degree b = card S ) iff b = (S,1) -bag ) set cS = canFS S; set f = b * (canFS S); A1: dom b = A by PARTFUN1:def_2; set g = (card S) |-> 1; A2: len (canFS S) = card S by Th3; A3: rng (canFS S) = S by FUNCT_2:def_3; then A4: dom (b * (canFS S)) = dom (canFS S) by A1, RELAT_1:27; then dom (b * (canFS S)) = Seg (len (canFS S)) by FINSEQ_1:def_3; then reconsider f = b * (canFS S) as FinSequence by FINSEQ_1:def_2; A5: len (canFS S) = len f by A4, FINSEQ_3:29; hereby ::_thesis: ( b = (S,1) -bag implies ( S = support b & degree b = card S ) ) set sb = (S,1) -bag ; assume that A6: S = support b and A7: degree b = card S ; ::_thesis: b = (S,1) -bag consider F being FinSequence of NAT such that A8: degree b = Sum F and A9: F = b * (canFS S) by A6, Def4; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_F_holds_ F_._i_<>_0 let i be Element of NAT ; ::_thesis: ( i in dom F implies F . i <> 0 ) assume i in dom F ; ::_thesis: F . i <> 0 then ( F . i = b . ((canFS S) . i) & (canFS S) . i in rng (canFS S) ) by A4, A9, FUNCT_1:3, FUNCT_1:12; hence F . i <> 0 by A6, PRE_POLY:def_7; ::_thesis: verum end; then A10: F = (len F) |-> 1 by A2, A5, A7, A8, A9, Th1; A11: support b = support ((S,1) -bag) by A6, Th8; now__::_thesis:_(_dom_b_=_dom_((S,1)_-bag)_&_(_for_x_being_set_st_x_in_dom_b_holds_ b_._x_=_((S,1)_-bag)_._x_)_) thus dom b = dom ((S,1) -bag) by A1, PARTFUN1:def_2; ::_thesis: for x being set st x in dom b holds b . b2 = ((S,1) -bag) . b2 let x be set ; ::_thesis: ( x in dom b implies b . b1 = ((S,1) -bag) . b1 ) assume x in dom b ; ::_thesis: b . b1 = ((S,1) -bag) . b1 percases ( x in support b or not x in support b ) ; supposeA12: x in support b ; ::_thesis: b . b1 = ((S,1) -bag) . b1 then A13: ((canFS S) ") . x in dom (canFS S) by A3, A6, FUNCT_1:32; then A14: ((canFS S) ") . x in Seg (len F) by A4, A9, FINSEQ_1:def_3; rng (canFS S) = support b by A6, FUNCT_2:def_3; hence b . x = b . ((canFS S) . (((canFS S) ") . x)) by A12, FUNCT_1:35 .= F . (((canFS S) ") . x) by A9, A13, FUNCT_1:13 .= 1 by A10, A14, FUNCOP_1:7 .= ((S,1) -bag) . x by A6, A12, Th7 ; ::_thesis: verum end; supposeA15: not x in support b ; ::_thesis: b . b1 = ((S,1) -bag) . b1 hence b . x = 0 by PRE_POLY:def_7 .= ((S,1) -bag) . x by A11, A15, PRE_POLY:def_7 ; ::_thesis: verum end; end; end; hence b = (S,1) -bag by FUNCT_1:2; ::_thesis: verum end; rng f c= NAT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT ) assume y in rng f ; ::_thesis: y in NAT 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 . ((canFS S) . x) by A16, FUNCT_1:12; hence y in NAT by A17; ::_thesis: verum end; then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4; assume A18: b = (S,1) -bag ; ::_thesis: ( S = support b & degree b = card S ) A19: rng (canFS S) = S by FUNCT_2:def_3; now__::_thesis:_(_len_f_=_card_S_&_len_((card_S)_|->_1)_=_card_S_&_(_for_i_being_Nat_st_i_in_dom_f_holds_ f_._i_=_((card_S)_|->_1)_._i_)_) thus len f = card S by A4, A2, FINSEQ_3:29; ::_thesis: ( len ((card S) |-> 1) = card S & ( for i being Nat st i in dom f holds f . i = ((card S) |-> 1) . i ) ) thus len ((card S) |-> 1) = card S by CARD_1:def_7; ::_thesis: for i being Nat st i in dom f holds f . i = ((card S) |-> 1) . i let i be Nat; ::_thesis: ( i in dom f implies f . i = ((card S) |-> 1) . i ) A20: dom f = Seg (card S) by A4, A2, FINSEQ_1:def_3; assume A21: i in dom f ; ::_thesis: f . i = ((card S) |-> 1) . i hence f . i = b . ((canFS S) . i) by FUNCT_1:12 .= 1 by A4, A19, A18, A21, Th7, FUNCT_1:3 .= ((card S) |-> 1) . i by A20, A21, FUNCOP_1:7 ; ::_thesis: verum end; then A22: f = (card S) |-> 1 by FINSEQ_2:9; thus S = support b by A18, Th8; ::_thesis: degree b = card S then degree b = Sum f by Def4; hence degree b = (card S) * 1 by A22, RVSUM_1:80 .= card S ; ::_thesis: verum end; theorem Th14: :: UPROOTS:14 for A being set for S being finite Subset of A for b being Rbag of A st support b c= S holds ex f being FinSequence of REAL st ( f = b * (canFS S) & Sum b = Sum f ) proof let A be set ; ::_thesis: for S being finite Subset of A for b being Rbag of A st support b c= S holds ex f being FinSequence of REAL st ( f = b * (canFS S) & Sum b = Sum f ) let S be finite Subset of A; ::_thesis: for b being Rbag of A st support b c= S holds ex f being FinSequence of REAL st ( f = b * (canFS S) & Sum b = Sum f ) let b be Rbag of A; ::_thesis: ( support b c= S implies ex f being FinSequence of REAL st ( f = b * (canFS S) & Sum b = Sum f ) ) assume A1: support b c= S ; ::_thesis: ex f being FinSequence of REAL st ( f = b * (canFS S) & Sum b = Sum f ) A2: card (support b) <= card S by A1, NAT_1:43; set cs = canFS (support b); A3: rng (canFS (support b)) = support b by FUNCT_2:def_3; set cS = canFS S; set f = b * (canFS S); len (canFS S) = card S by Th3; then A4: dom (canFS S) = Seg (card S) by FINSEQ_1:def_3; len (canFS (support b)) = card (support b) by Th3; then A5: dom (canFS (support b)) = 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 * (canFS (support b)) 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 (canFS S) = S by FUNCT_2:def_3; then A12: dom (b * (canFS S)) = Seg (card S) by A4, A8, RELAT_1:27; then reconsider f = b * (canFS S) 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 = f as FinSequence of REAL by FINSEQ_1:def_4; take f ; ::_thesis: ( f = b * (canFS S) & Sum b = Sum f ) thus f = b * (canFS S) ; ::_thesis: Sum b = Sum f percases ( card (support b) < card S or card (support b) = card S ) by A2, XXREAL_0:1; supposeA13: card (support b) < card S ; ::_thesis: Sum b = Sum f set dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ; A14: now__::_thesis:_not__{__j_where_j_is_Element_of_NAT_:_(_j_in_dom_f_&_f_._j_=_0_)__}__is_empty consider x being set such that A15: ( ( x in support b & not x in S ) or ( x in S & not x in support b ) ) by A13, TARSKI:1; consider j being set such that A16: j in dom (canFS S) and A17: (canFS S) . j = x by A1, A11, A15, FUNCT_1:def_3; reconsider j = 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 { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } by A4, A12, A16; hence not { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } is empty ; ::_thesis: verum end; reconsider gr = g as FinSequence of REAL ; A18: { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } or x in dom f ) assume x in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ; ::_thesis: x in dom f then ex j being Element of NAT st ( x = j & j in dom f & f . j = 0 ) ; hence x in dom f ; ::_thesis: verum end; then reconsider dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } as non empty finite 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; set F = gr ^ (d |-> 0); ( 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 " ; reconsider cdi = cdd " as Function of dd,(Seg (card dd)) by Th5; reconsider cdi = cdi as Function of dd,NAT by FUNCT_2:7; deffunc H1( set ) -> Element of NAT = (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 = H1(x) from FUNCT_1:sch_3(); set p = (((canFS (support b)) ") * (canFS S)) +* z; A22: dom cdi = dd by FUNCT_2:def_1; set cSr = (canFS S) | ((dom f) \ dd); now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_((canFS_S)_|_((dom_f)_\_dd))_implies_y_in_support_b_)_&_(_y_in_support_b_implies_y_in_rng_((canFS_S)_|_((dom_f)_\_dd))_)_) let y be set ; ::_thesis: ( ( y in rng ((canFS S) | ((dom f) \ dd)) implies y in support b ) & ( y in support b implies y in rng ((canFS S) | ((dom f) \ dd)) ) ) hereby ::_thesis: ( y in support b implies y in rng ((canFS S) | ((dom f) \ dd)) ) assume y in rng ((canFS S) | ((dom f) \ dd)) ; ::_thesis: y in support b then consider x being set such that A23: x in dom ((canFS S) | ((dom f) \ dd)) and A24: y = ((canFS S) | ((dom f) \ dd)) . x by FUNCT_1:def_3; A25: ((canFS S) | ((dom f) \ dd)) . x = (canFS S) . x by A23, FUNCT_1:47; x in dom (canFS S) 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 (canFS S) by A23, RELAT_1:57; then b . ((canFS S) . j) <> 0 by A27, FUNCT_1:13; hence y in support b by A24, A25, PRE_POLY:def_7; ::_thesis: verum end; assume A28: y in support b ; ::_thesis: y in rng ((canFS S) | ((dom f) \ dd)) then consider x being set such that A29: x in dom (canFS S) and A30: y = (canFS S) . x by A1, A11, FUNCT_1:def_3; now__::_thesis:_not_x_in_dd assume x in dd ; ::_thesis: contradiction then consider j being Element of NAT such that A31: j = x and A32: ( j in dom f & f . j = 0 ) ; 0 = b . ((canFS S) . j) by A4, A12, A32, FUNCT_1:13; hence contradiction by A28, A30, A31, PRE_POLY:def_7; ::_thesis: verum end; then x in (dom f) \ dd by A4, A12, A29, XBOOLE_0:def_5; hence y in rng ((canFS S) | ((dom f) \ dd)) by A29, A30, FUNCT_1:50; ::_thesis: verum end; then A33: rng ((canFS S) | ((dom f) \ dd)) = support b by TARSKI:1; ((findom f) \ dd) /\ (dom f) = (dom f) \ dd by XBOOLE_1:28; then ( (canFS S) | ((dom f) \ dd) is one-to-one & dom ((canFS S) | ((dom f) \ dd)) = (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__::_thesis:_not_(dom_(((canFS_(support_b))_")_*_(canFS_S)))_/\_(dom_z)_<>_{} A37: dom ((canFS (support b)) ") = support b by A3, FUNCT_1:33; assume (dom (((canFS (support b)) ") * (canFS S))) /\ (dom z) <> {} ; ::_thesis: contradiction then consider x being set such that A38: x in (dom (((canFS (support b)) ") * (canFS S))) /\ (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 (((canFS (support b)) ") * (canFS S)) by A38, XBOOLE_0:def_4; then j in dom (canFS S) by A39, FUNCT_1:11; then f . j = b . ((canFS S) . j) by FUNCT_1:13; then not (canFS S) . j in support b by A40, PRE_POLY:def_7; hence contradiction by A41, A39, A37, FUNCT_1:11; ::_thesis: verum end; len (gr ^ (d |-> 0)) = (len g) + (len (d |-> 0)) by FINSEQ_1:22 .= card S by A10, A19, CARD_1:def_7 ; then A42: dom (gr ^ (d |-> 0)) = Seg (card S) by FINSEQ_1:def_3; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(dom_(((canFS_(support_b))_")_*_(canFS_S)))_\/_(dom_z)_implies_x_in_dom_(gr_^_(d_|->_0))_)_&_(_x_in_dom_(gr_^_(d_|->_0))_implies_x_in_(dom_(((canFS_(support_b))_")_*_(canFS_S)))_\/_(dom_z)_)_) let x be set ; ::_thesis: ( ( x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) implies x in dom (gr ^ (d |-> 0)) ) & ( x in dom (gr ^ (d |-> 0)) implies b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ) ) hereby ::_thesis: ( x in dom (gr ^ (d |-> 0)) implies b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ) assume A43: x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ; ::_thesis: x in dom (gr ^ (d |-> 0)) percases ( x in dom (((canFS (support b)) ") * (canFS S)) or x in dom z ) by A43, XBOOLE_0:def_3; suppose x in dom (((canFS (support b)) ") * (canFS S)) ; ::_thesis: x in dom (gr ^ (d |-> 0)) hence x in dom (gr ^ (d |-> 0)) by A4, A42, FUNCT_1:11; ::_thesis: verum end; suppose x in dom z ; ::_thesis: x in dom (gr ^ (d |-> 0)) hence x in dom (gr ^ (d |-> 0)) by A12, A42, A18, A20; ::_thesis: verum end; end; end; assume A44: x in dom (gr ^ (d |-> 0)) ; ::_thesis: b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) then reconsider i = x as Element of NAT ; percases ( f . x = 0 or f . x <> 0 ) ; suppose f . x = 0 ; ::_thesis: b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) then i in dom z by A12, A42, A20, A44; hence x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA45: f . x <> 0 ; ::_thesis: b1 in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) f . i = b . ((canFS S) . i) by A4, A42, A44, FUNCT_1:13; then (canFS S) . i in support b by A45, PRE_POLY:def_7; then (canFS S) . i in dom ((canFS (support b)) ") by A3, FUNCT_1:33; then i in dom (((canFS (support b)) ") * (canFS S)) by A4, A42, A44, FUNCT_1:11; hence x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; then A46: (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) = dom (gr ^ (d |-> 0)) by TARSKI:1; then A47: dom ((((canFS (support b)) ") * (canFS S)) +* z) = dom (gr ^ (d |-> 0)) 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng z or y in Seg (card S) ) assume y in rng z ; ::_thesis: y in Seg (card S) 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 y in Seg (card S) by A19, A54, A55, FINSEQ_1:1; ::_thesis: verum end; A56: now__::_thesis:_for_x_being_set_st_x_in_dom_(gr_^_(d_|->_0))_holds_ ((((canFS_(support_b))_")_*_(canFS_S))_+*_z)_._x_in_dom_(gr_^_(d_|->_0)) let x be set ; ::_thesis: ( x in dom (gr ^ (d |-> 0)) implies ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0)) ) assume A57: x in dom (gr ^ (d |-> 0)) ; ::_thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0)) percases ( x in dom (((canFS (support b)) ") * (canFS S)) or x in dom z ) by A46, A57, XBOOLE_0:def_3; supposeA58: x in dom (((canFS (support b)) ") * (canFS S)) ; ::_thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0)) then (((canFS (support b)) ") * (canFS S)) . x in rng (((canFS (support b)) ") * (canFS S)) by FUNCT_1:3; then (((canFS (support b)) ") * (canFS S)) . x in rng ((canFS (support b)) ") by FUNCT_1:14; then A59: (((canFS (support b)) ") * (canFS S)) . x in dom (canFS (support b)) by FUNCT_1:33; not x in dom z by A36, A58, XBOOLE_0:def_4; then A60: ((((canFS (support b)) ") * (canFS S)) +* z) . x = (((canFS (support b)) ") * (canFS S)) . x by FUNCT_4:11; Seg (card (support b)) c= Seg (card S) by A2, FINSEQ_1:5; hence ((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> 0)) by A5, A42, A60, A59; ::_thesis: verum end; suppose x in dom z ; ::_thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b1 in dom (gr ^ (d |-> 0)) then ( ((((canFS (support b)) ") * (canFS S)) +* z) . x = z . x & z . x in rng z ) by FUNCT_1:3, FUNCT_4:13; hence ((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> 0)) by A42, A50; ::_thesis: verum end; end; end; A61: dom ((((canFS (support b)) ") * (canFS S)) +* z) = (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by FUNCT_4:def_1; reconsider p = (((canFS (support b)) ") * (canFS S)) +* z as Function of (dom (gr ^ (d |-> 0))),(dom (gr ^ (d |-> 0))) by A47, A56, FUNCT_2:3; len (d |-> 0) = d by CARD_1:def_7; then A62: dom (d |-> 0) = Seg d by FINSEQ_1:def_3; A63: rng cdd = dd by FUNCT_2:def_3; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_rng_p_implies_x_in_dom_(gr_^_(d_|->_0))_)_&_(_x_in_dom_(gr_^_(d_|->_0))_implies_x_in_rng_p_)_) let x be set ; ::_thesis: ( ( x in rng p implies x in dom (gr ^ (d |-> 0)) ) & ( x in dom (gr ^ (d |-> 0)) implies b1 in rng p ) ) hereby ::_thesis: ( x in dom (gr ^ (d |-> 0)) implies b1 in rng p ) assume x in rng p ; ::_thesis: x in dom (gr ^ (d |-> 0)) then consider a being set such that A64: a in dom p and A65: x = p . a by FUNCT_1:def_3; percases ( a in dom (((canFS (support b)) ") * (canFS S)) or a in dom z ) by A64, FUNCT_4:12; supposeA66: a in dom (((canFS (support b)) ") * (canFS S)) ; ::_thesis: x in dom (gr ^ (d |-> 0)) then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11; then ((canFS (support b)) ") . ((canFS S) . a) in rng ((canFS (support b)) ") by FUNCT_1:3; then A67: ((canFS (support b)) ") . ((canFS S) . a) in dom (canFS (support b)) by FUNCT_1:33; not a in dom z by A36, A66, XBOOLE_0:def_4; then A68: p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11 .= ((canFS (support b)) ") . ((canFS S) . a) by A66, FUNCT_1:12 ; dom (canFS (support b)) c= dom (gr ^ (d |-> 0)) by A5, A2, A42, FINSEQ_1:5; hence x in dom (gr ^ (d |-> 0)) by A65, A68, A67; ::_thesis: verum end; suppose a in dom z ; ::_thesis: x in dom (gr ^ (d |-> 0)) then ( z . a in rng z & p . a = z . a ) by FUNCT_1:3, FUNCT_4:13; hence x in dom (gr ^ (d |-> 0)) by A42, A50, A65; ::_thesis: verum end; end; end; assume A69: x in dom (gr ^ (d |-> 0)) ; ::_thesis: b1 in rng p then reconsider j = x as Element of NAT ; percases ( j in dom gr or ex n being Nat st ( n in dom (d |-> 0) & j = (len gr) + n ) ) by A69, FINSEQ_1:25; supposeA70: j in dom gr ; ::_thesis: b1 in rng p then A71: (canFS (support b)) . j in support b by A5, A3, A9, FUNCT_1:3; then A72: ((canFS S) ") . ((canFS (support b)) . j) in Seg (card S) by A1, A4, A11, FUNCT_1:32; now__::_thesis:_not_((canFS_S)_")_._((canFS_(support_b))_._j)_in_dom_z assume ((canFS S) ") . ((canFS (support b)) . j) in dom z ; ::_thesis: contradiction then A73: ex k being Element of NAT st ( k = ((canFS S) ") . ((canFS (support b)) . j) & k in dom f & f . k = 0 ) by A20; (b * (canFS S)) . (((canFS S) ") . ((canFS (support b)) . j)) = b . ((canFS S) . (((canFS S) ") . ((canFS (support b)) . j))) by A4, A72, FUNCT_1:13 .= b . ((canFS (support b)) . j) by A1, A11, A71, FUNCT_1:35 ; hence contradiction by A71, A73, PRE_POLY:def_7; ::_thesis: verum end; then p . (((canFS S) ") . ((canFS (support b)) . j)) = (((canFS (support b)) ") * (canFS S)) . (((canFS S) ") . ((canFS (support b)) . j)) by FUNCT_4:11 .= ((canFS (support b)) ") . ((canFS S) . (((canFS S) ") . ((canFS (support b)) . j))) by A4, A72, FUNCT_1:13 .= ((canFS (support b)) ") . ((canFS (support b)) . 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; ::_thesis: verum end; suppose ex n being Nat st ( n in dom (d |-> 0) & j = (len gr) + n ) ; ::_thesis: b1 in rng p then consider n being Nat such that A74: n in dom (d |-> 0) 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; ::_thesis: verum end; end; end; then A77: rng p = dom (gr ^ (d |-> 0)) by TARSKI:1; then A78: dom ((gr ^ (d |-> 0)) * p) = dom (gr ^ (d |-> 0)) by A47, RELAT_1:27; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_((gr_^_(d_|->_0))_*_p)_._x let x be set ; ::_thesis: ( x in dom f implies f . b1 = ((gr ^ (d |-> 0)) * p) . b1 ) assume A79: x in dom f ; ::_thesis: f . b1 = ((gr ^ (d |-> 0)) * p) . b1 percases ( f . x = 0 or f . x <> 0 ) ; supposeA80: f . x = 0 ; ::_thesis: f . b1 = ((gr ^ (d |-> 0)) * p) . b1 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 = (d |-> 0) . cdix by A80 .= (gr ^ (d |-> 0)) . px by A10, A19, A62, A35, A82, A84, A83, FINSEQ_1:def_7 .= ((gr ^ (d |-> 0)) * p) . x by A12, A42, A78, A79, FUNCT_1:12 ; ::_thesis: verum end; supposeA85: f . x <> 0 ; ::_thesis: f . b1 = ((gr ^ (d |-> 0)) * p) . b1 reconsider px = p . x as Element of NAT ; f . x = b . ((canFS S) . x) by A79, FUNCT_1:12; then (canFS S) . x in support b by A85, PRE_POLY:def_7; then A86: (canFS S) . x in rng (canFS (support b)) by FUNCT_2:def_3; then A87: ((canFS (support b)) ") . ((canFS S) . x) in dom (canFS (support b)) by FUNCT_1:32; now__::_thesis:_not_x_in_dd assume x in dd ; ::_thesis: contradiction then ex j being Element of NAT st ( j = x & j in dom f & f . j = 0 ) ; hence contradiction by A85; ::_thesis: verum end; then A88: p . x = (((canFS (support b)) ") * (canFS S)) . x by A20, FUNCT_4:11 .= ((canFS (support b)) ") . ((canFS S) . x) by A4, A12, A79, FUNCT_1:13 ; thus f . x = b . ((canFS S) . x) by A79, FUNCT_1:12 .= b . ((canFS (support b)) . px) by A86, A88, FUNCT_1:32 .= g . px by A7, A87, A88, FUNCT_1:13 .= (gr ^ (d |-> 0)) . px by A5, A9, A87, A88, FINSEQ_1:def_7 .= ((gr ^ (d |-> 0)) * p) . x by A12, A42, A78, A79, FUNCT_1:12 ; ::_thesis: verum end; end; end; then A89: f = (gr ^ (d |-> 0)) * 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 ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 p or not c in proj1 p or not p . a = p . c or a = c ) assume that A91: ( a in dom p & c in dom p ) and A92: p . a = p . c ; ::_thesis: a = c percases ( ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom (((canFS (support b)) ") * (canFS S)) ) or ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom z ) or ( a in dom z & c in dom (((canFS (support b)) ") * (canFS S)) ) or ( a in dom z & c in dom z ) ) by A61, A91, XBOOLE_0:def_3; supposeA93: ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom (((canFS (support b)) ") * (canFS S)) ) ; ::_thesis: a = c then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11; then (canFS S) . a in rng (canFS (support b)) by FUNCT_1:33; then A94: (canFS (support b)) . (((canFS (support b)) ") . ((canFS S) . a)) = (canFS S) . a by FUNCT_1:35; a in dom (canFS S) by A93, FUNCT_1:11; then A95: ((canFS S) ") . ((canFS S) . a) = a by FUNCT_1:34; (canFS S) . c in dom ((canFS (support b)) ") by A93, FUNCT_1:11; then A96: (canFS S) . c in rng (canFS (support b)) by FUNCT_1:33; not c in dom z by A36, A93, XBOOLE_0:def_4; then A97: p . c = (((canFS (support b)) ") * (canFS S)) . c by FUNCT_4:11 .= ((canFS (support b)) ") . ((canFS S) . c) by A93, FUNCT_1:12 ; A98: c in dom (canFS S) by A93, FUNCT_1:11; not a in dom z by A36, A93, XBOOLE_0:def_4; then p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11 .= ((canFS (support b)) ") . ((canFS S) . a) by A93, FUNCT_1:12 ; then ((canFS S) ") . ((canFS S) . a) = ((canFS S) ") . ((canFS S) . c) by A92, A97, A94, A96, FUNCT_1:35; hence a = c by A95, A98, FUNCT_1:34; ::_thesis: verum end; supposeA99: ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom z ) ; ::_thesis: a = c then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11; then ((canFS (support b)) ") . ((canFS S) . a) in rng ((canFS (support b)) ") by FUNCT_1:3; then A100: ((canFS (support b)) ") . ((canFS S) . a) in dom (canFS (support b)) by FUNCT_1:33; not a in dom z by A36, A99, XBOOLE_0:def_4; then A101: p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11 .= ((canFS (support b)) ") . ((canFS S) . 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 + (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 a = c by A49, A102, FINSEQ_1:1; ::_thesis: verum end; supposeA103: ( a in dom z & c in dom (((canFS (support b)) ") * (canFS S)) ) ; ::_thesis: a = c then (canFS S) . c in dom ((canFS (support b)) ") by FUNCT_1:11; then ((canFS (support b)) ") . ((canFS S) . c) in rng ((canFS (support b)) ") by FUNCT_1:3; then A104: ((canFS (support b)) ") . ((canFS S) . c) in dom (canFS (support b)) by FUNCT_1:33; not c in dom z by A36, A103, XBOOLE_0:def_4; then A105: p . c = (((canFS (support b)) ") * (canFS S)) . c by FUNCT_4:11 .= ((canFS (support b)) ") . ((canFS S) . 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 + (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 a = c by A49, A106, FINSEQ_1:1; ::_thesis: verum end; supposeA107: ( a in dom z & c in dom z ) ; ::_thesis: a = c 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 a = c by A22, A20, A92, A107, A109, A108, FUNCT_1:def_4; ::_thesis: verum end; end; end; Sum (d |-> 0) = 0 by RVSUM_1:81; then A110: Sum gr = (Sum gr) + (Sum (d |-> 0)) .= Sum (gr ^ (d |-> 0)) by RVSUM_1:75 ; p is onto by A77, FUNCT_2:def_3; hence Sum b = Sum f by A6, A90, A89, A110, FINSOP_1:7; ::_thesis: verum end; suppose card (support b) = card S ; ::_thesis: Sum b = Sum f hence Sum b = Sum f by A1, A6, A7, PRE_POLY:8; ::_thesis: verum end; end; end; theorem Th15: :: UPROOTS:15 for A being set for b, b1, b2 being Rbag of A st b = b1 + b2 holds Sum b = (Sum b1) + (Sum b2) proof let A be set ; ::_thesis: for b, b1, b2 being Rbag of A st b = b1 + b2 holds Sum b = (Sum b1) + (Sum b2) let b, b1, b2 be Rbag of A; ::_thesis: ( b = b1 + b2 implies Sum b = (Sum b1) + (Sum b2) ) 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 = (support b1) \/ (support b2) 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 (canFS SS) = SS by FUNCT_2:def_3; then A7: dom f1r = dom (canFS SS) by A3, A4, RELAT_1:27; assume A8: b = b1 + b2 ; ::_thesis: Sum b = (Sum b1) + (Sum b2) then support b 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 (canFS SS) 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 (canFS SS) by A1, A13, A6, RELAT_1:27; A16: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_f1r_holds_ f_._k_=_(f1r_/._k)_+_(f2r_/._k) let k be Element of NAT ; ::_thesis: ( k in dom f1r implies f . k = (f1r /. k) + (f2r /. k) ) assume A17: k in dom f1r ; ::_thesis: f . k = (f1r /. k) + (f2r /. k) A18: f1r /. k = f1r . k by A17, PARTFUN1:def_6 .= b1 . ((canFS SS) . k) by A4, A17, FUNCT_1:12 ; A19: f . k = b . ((canFS SS) . k) by A9, A11, A7, A17, FUNCT_1:12; f2r /. k = f2r . k by A7, A15, A17, PARTFUN1:def_6 .= b2 . ((canFS SS) . k) by A13, A7, A15, A17, FUNCT_1:12 ; hence f . k = (f1r /. k) + (f2r /. k) by A8, A18, A19, PRE_POLY:def_5; ::_thesis: verum end; len f1r = len f2r by A7, A15, FINSEQ_3:29; hence Sum b = (Sum b1) + (Sum b2) by A10, A5, A14, A12, A16, INTEGRA1:21; ::_thesis: verum end; theorem Th16: :: UPROOTS:16 for L being non empty unital associative commutative multMagma for f, g being FinSequence of L for p being Permutation of (dom f) st g = f * p holds Product g = Product f proof let L be non empty unital associative commutative multMagma ; ::_thesis: for f, g being FinSequence of L for p being Permutation of (dom f) st g = f * p holds Product g = Product f let f, g be FinSequence of L; ::_thesis: for p being Permutation of (dom f) st g = f * p holds Product g = Product f let p be Permutation of (dom f); ::_thesis: ( g = f * p implies Product g = Product f ) assume A1: g = f * p ; ::_thesis: Product g = Product f set mL = the multF of L; ( the multF of L is commutative & the multF of L is associative ) by MONOID_0:def_11; hence Product g = Product f by A1, FINSOP_1:7; ::_thesis: verum end; begin definition let L be non empty ZeroStr ; let p be Polynomial of L; attrp is non-zero means :Def5: :: UPROOTS:def 5 p <> 0_. L; end; :: deftheorem Def5 defines non-zero UPROOTS:def_5_:_ for L being non empty ZeroStr for p being Polynomial of L holds ( p is non-zero iff p <> 0_. L ); theorem Th17: :: UPROOTS:17 for L being non empty ZeroStr for p being Polynomial of L holds ( p is non-zero iff len p > 0 ) proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L holds ( p is non-zero iff len p > 0 ) let p be Polynomial of L; ::_thesis: ( p is non-zero iff len p > 0 ) hereby ::_thesis: ( len p > 0 implies p is non-zero ) assume p is non-zero ; ::_thesis: len p > 0 then p <> 0_. L by Def5; then len p <> 0 by POLYNOM4:5; hence len p > 0 ; ::_thesis: verum end; assume len p > 0 ; ::_thesis: p is non-zero then p <> 0_. L by POLYNOM4:3; hence p is non-zero by Def5; ::_thesis: verum end; registration let L be non trivial ZeroStr ; cluster Relation-like NAT -defined the carrier of L -valued Function-like non empty total quasi_total finite-Support non-zero for Element of bool [:NAT, the carrier of L:]; existence ex b1 being Polynomial of L st b1 is non-zero proof set a = the Element of NonZero L; reconsider a = the Element of NonZero L as Element of L ; take p = <%a%>; ::_thesis: p is non-zero 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 p is non-zero by Def5; ::_thesis: verum end; end; registration let L be non empty non degenerated multLoopStr_0 ; let x be Element of L; cluster<%x,(1. L)%> -> non-zero ; correctness coherence <%x,(1. L)%> is non-zero ; proof len <%x,(1. L)%> = 2 by POLYNOM5:40; hence <%x,(1. L)%> is non-zero by Th17; ::_thesis: verum end; end; theorem Th18: :: UPROOTS:18 for L being non empty ZeroStr for p being Polynomial of L st len p > 0 holds p . ((len p) -' 1) <> 0. L proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L st len p > 0 holds p . ((len p) -' 1) <> 0. L let p be Polynomial of L; ::_thesis: ( len p > 0 implies p . ((len p) -' 1) <> 0. L ) assume len p > 0 ; ::_thesis: p . ((len p) -' 1) <> 0. L 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 p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10; ::_thesis: verum end; theorem Th19: :: UPROOTS:19 for L being non empty ZeroStr for p being AlgSequence of L st len p = 1 holds ( p = <%(p . 0)%> & p . 0 <> 0. L ) proof let L be non empty ZeroStr ; ::_thesis: for p being AlgSequence of L st len p = 1 holds ( p = <%(p . 0)%> & p . 0 <> 0. L ) let p be AlgSequence of L; ::_thesis: ( len p = 1 implies ( p = <%(p . 0)%> & p . 0 <> 0. L ) ) assume A1: len p = 1 ; ::_thesis: ( p = <%(p . 0)%> & p . 0 <> 0. L ) thus p = <%(p . 0)%> by A1, ALGSEQ_1:def_5; ::_thesis: p . 0 <> 0. L hence p . 0 <> 0. L by A1, ALGSEQ_1:14; ::_thesis: verum end; theorem Th20: :: UPROOTS:20 for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L holds p *' (0_. L) = 0_. L proof let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p *' (0_. L) = 0_. L let p be Polynomial of L; ::_thesis: p *' (0_. L) = 0_. L now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(0_._L))_._i_=_(0_._L)_._i let i be Element of NAT ; ::_thesis: (p *' (0_. L)) . i = (0_. L) . i consider r being FinSequence of L such that len r = i + 1 and A1: (p *' (0_. L)) . i = Sum r and A2: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by POLYNOM3:def_9; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r implies r . k = 0. L ) assume k in dom r ; ::_thesis: r . k = 0. L 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 ; ::_thesis: verum end; hence (p *' (0_. L)) . i = 0. L by A1, POLYNOM3:1 .= (0_. L) . i by FUNCOP_1:7 ; ::_thesis: verum end; hence p *' (0_. L) = 0_. L by FUNCT_2:63; ::_thesis: verum end; registration cluster non empty non degenerated right_complementable unital associative commutative distributive Abelian add-associative right_zeroed domRing-like algebraic-closed for doubleLoopStr ; existence ex b1 being non empty unital doubleLoopStr st ( b1 is algebraic-closed & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is distributive & b1 is domRing-like & not b1 is degenerated ) proof take F_Complex ; ::_thesis: ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is domRing-like & not F_Complex is degenerated ) thus ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is domRing-like & not F_Complex is degenerated ) ; ::_thesis: verum end; end; theorem Th21: :: UPROOTS:21 for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being Polynomial of L holds ( not p *' q = 0_. L or p = 0_. L or q = 0_. L ) proof let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being Polynomial of L holds ( not p *' q = 0_. L or p = 0_. L or q = 0_. L ) let p, q be Polynomial of L; ::_thesis: ( not p *' q = 0_. L or p = 0_. L or q = 0_. L ) assume that A1: p *' q = 0_. L and A2: p <> 0_. L and A3: q <> 0_. L ; ::_thesis: contradiction 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 + 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 = lp1, lq1 = 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 = (lp1 + lq1) + 1 and A10: (p *' q) . (lp1 + lq1) = Sum r and A11: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . (((lp1 + lq1) + 1) -' k)) by POLYNOM3:def_9; A12: ((lp1 + lq1) + 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__::_thesis:_for_k_being_Nat_st_k_in_dom_r_&_k_<>_len_p_holds_ r_._k_=_0._L let k be Nat; ::_thesis: ( k in dom r & k <> len p implies r . b1 = 0. L ) assume that A14: k in dom r and A15: k <> len p ; ::_thesis: r . b1 = 0. L reconsider k1 = k as Element of NAT by ORDINAL1:def_12; A16: r . k1 = (p . (k1 -' 1)) * (q . (((lp1 + lq1) + 1) -' k1)) by A11, A14; percases ( k < len p or k > len p ) by A15, XXREAL_0:1; suppose k < len p ; ::_thesis: r . b1 = 0. L 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; ((lp1 + lq1) + 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 ; ::_thesis: verum end; suppose k > len p ; ::_thesis: r . b1 = 0. L 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 . (((lp1 + lq1) + 1) -' k)) by A16, ALGSEQ_1:8 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; end; end; then Sum r = r . (len p) by A13, MATRIX_3:12 .= (p . ((len p) -' 1)) * (q . (((lp1 + lq1) + 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; ::_thesis: verum end; registration let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; cluster Polynom-Ring L -> domRing-like ; correctness coherence Polynom-Ring L is domRing-like ; proof set PRL = Polynom-Ring L; let x, y be Element of (Polynom-Ring L); :: according to VECTSP_2:def_1 ::_thesis: ( not x * y = 0. (Polynom-Ring L) or x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) ) reconsider xp = x, yp = y as Polynomial of L by POLYNOM3:def_10; A1: 0_. L = 0. (Polynom-Ring L) by POLYNOM3:def_10; assume x * y = 0. (Polynom-Ring L) ; ::_thesis: ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) ) then xp *' yp = 0_. L by A1, POLYNOM3:def_10; hence ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) ) by A1, Th21; ::_thesis: verum end; end; registration let L be domRing; let p, q be non-zero Polynomial of L; clusterp *' q -> non-zero ; correctness coherence p *' q is non-zero ; proof ( p <> 0_. L & q <> 0_. L ) by Def5; then p *' q <> 0_. L by Th21; hence p *' q is non-zero by Def5; ::_thesis: verum end; end; theorem :: UPROOTS:22 for L being non degenerated comRing for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q) proof let L be non degenerated comRing; ::_thesis: for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q) let p, q be Polynomial of L; ::_thesis: (Roots p) \/ (Roots q) c= Roots (p *' q) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Roots p) \/ (Roots q) or x in Roots (p *' q) ) assume A1: x in (Roots p) \/ (Roots q) ; ::_thesis: x in Roots (p *' q) percases ( x in Roots p or x in Roots q ) by A1, XBOOLE_0:def_3; supposeA2: x in Roots p ; ::_thesis: x in Roots (p *' q) 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 x in Roots (p *' q) by POLYNOM5:def_9; ::_thesis: verum end; supposeA3: x in Roots q ; ::_thesis: x in Roots (p *' 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 x in Roots (p *' q) by POLYNOM5:def_9; ::_thesis: verum end; end; end; theorem Th23: :: UPROOTS:23 for L being domRing for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q) proof let L be domRing; ::_thesis: for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q) let p, q be Polynomial of L; ::_thesis: Roots (p *' q) = (Roots p) \/ (Roots q) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Roots_(p_*'_q)_implies_x_in_(Roots_p)_\/_(Roots_q)_)_&_(_x_in_(Roots_p)_\/_(Roots_q)_implies_x_in_Roots_(p_*'_q)_)_) let x be set ; ::_thesis: ( ( x in Roots (p *' q) implies x in (Roots p) \/ (Roots q) ) & ( x in (Roots p) \/ (Roots q) implies b1 in Roots (p *' q) ) ) hereby ::_thesis: ( x in (Roots p) \/ (Roots q) implies b1 in Roots (p *' q) ) assume A1: x in Roots (p *' q) ; ::_thesis: x in (Roots p) \/ (Roots 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; percases ( eval (p,a) = 0. L or eval (q,a) = 0. L ) by A2, VECTSP_2:def_1; suppose eval (p,a) = 0. L ; ::_thesis: x in (Roots p) \/ (Roots q) 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; ::_thesis: verum end; suppose eval (q,a) = 0. L ; ::_thesis: x in (Roots p) \/ (Roots q) 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; ::_thesis: verum end; end; end; assume A3: x in (Roots p) \/ (Roots q) ; ::_thesis: b1 in Roots (p *' q) percases ( x in Roots p or x in Roots q ) by A3, XBOOLE_0:def_3; supposeA4: x in Roots p ; ::_thesis: b1 in Roots (p *' q) 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; ::_thesis: verum end; supposeA5: x in Roots q ; ::_thesis: b1 in Roots (p *' 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; ::_thesis: verum end; end; end; hence Roots (p *' q) = (Roots p) \/ (Roots q) by TARSKI:1; ::_thesis: verum end; theorem Th24: :: UPROOTS:24 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L for pc being Element of (Polynom-Ring L) st p = pc holds - p = - pc proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for pc being Element of (Polynom-Ring L) st p = pc holds - p = - pc let p be Polynomial of L; ::_thesis: for pc being Element of (Polynom-Ring L) st p = pc holds - p = - pc let pc be Element of (Polynom-Ring L); ::_thesis: ( p = pc implies - p = - pc ) assume A1: p = pc ; ::_thesis: - p = - pc set PRL = Polynom-Ring L; reconsider mpc = - p as Element of (Polynom-Ring L) by POLYNOM3:def_10; p + (- p) = p - p .= 0_. L by POLYNOM3:29 ; then pc + mpc = 0_. L by A1, POLYNOM3:def_10 .= 0. (Polynom-Ring L) by POLYNOM3:def_10 ; hence - p = - pc by RLVECT_1:def_10; ::_thesis: verum end; theorem Th25: :: UPROOTS:25 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds p - q = pc - qc proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds p - q = pc - qc let p, q be Polynomial of L; ::_thesis: for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds p - q = pc - qc let pc, qc be Element of (Polynom-Ring L); ::_thesis: ( p = pc & q = qc implies p - q = pc - qc ) assume that A1: p = pc and A2: q = qc ; ::_thesis: p - q = pc - qc - q = - qc by A2, Th24; hence p - q = pc - qc by A1, POLYNOM3:def_10; ::_thesis: verum end; theorem Th26: :: UPROOTS:26 for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r) proof let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r) let p, q, r be Polynomial of L; ::_thesis: (p *' q) - (p *' r) = p *' (q - r) set PRL = Polynom-Ring L; reconsider pc = p, qc = q, rc = r as Element of (Polynom-Ring L) 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 ; ::_thesis: verum end; theorem Th27: :: UPROOTS:27 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L st p - q = 0_. L holds p = q proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st p - q = 0_. L holds p = q let q, r be Polynomial of L; ::_thesis: ( q - r = 0_. L implies q = r ) set PRL = Polynom-Ring L; reconsider qc = q, rc = r as Element of (Polynom-Ring L) by POLYNOM3:def_10; assume A1: q - r = 0_. L ; ::_thesis: q = r 0_. L = 0. (Polynom-Ring L) by POLYNOM3:def_10; then qc - rc = 0. (Polynom-Ring L) by A1, Th25; hence q = r by VECTSP_1:27; ::_thesis: verum end; theorem Th28: :: UPROOTS:28 for L being non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds q = r proof let L be non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds q = r let p, q, r be Polynomial of L; ::_thesis: ( p <> 0_. L & p *' q = p *' r implies q = r ) assume A1: p <> 0_. L ; ::_thesis: ( not p *' q = p *' r or q = r ) assume p *' q = p *' r ; ::_thesis: q = 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 q = r by Th27; ::_thesis: verum end; theorem Th29: :: UPROOTS:29 for L being domRing for n being Element of NAT for p being Polynomial of L st p <> 0_. L holds p `^ n <> 0_. L proof let L be domRing; ::_thesis: for n being Element of NAT for p being Polynomial of L st p <> 0_. L holds p `^ n <> 0_. L let n be Element of NAT ; ::_thesis: for p being Polynomial of L st p <> 0_. L holds p `^ n <> 0_. L let p be Polynomial of L; ::_thesis: ( p <> 0_. L implies p `^ n <> 0_. L ) defpred S1[ Element of NAT ] means p `^ $1 <> 0_. L; assume A1: p <> 0_. L ; ::_thesis: p `^ n <> 0_. L A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] p `^ (n + 1) = (p `^ n) *' p by POLYNOM5:19; hence S1[n + 1] by A1, A3, Th21; ::_thesis: verum end; ( (1_. L) . 0 = 1. L & (0_. L) . 0 = 0. L ) by FUNCOP_1:7, POLYNOM3:30; then A4: S1[ 0 ] by POLYNOM5:15; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence p `^ n <> 0_. L ; ::_thesis: verum end; theorem Th30: :: UPROOTS:30 for L being comRing for i, j being Element of NAT for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j) proof let L be comRing; ::_thesis: for i, j being Element of NAT for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j) let i, j be Element of NAT ; ::_thesis: for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j) let p be Polynomial of L; ::_thesis: (p `^ i) *' (p `^ j) = p `^ (i + j) defpred S1[ Element of NAT ] means (p `^ i) *' (p `^ $1) = p `^ (i + $1); A1: for j being Element of NAT st S1[j] holds S1[j + 1] proof let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] ) assume A2: S1[j] ; ::_thesis: S1[j + 1] (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 S1[j + 1] ; ::_thesis: verum end; (p `^ i) *' (p `^ 0) = (p `^ i) *' (1_. L) by POLYNOM5:15 .= p `^ (i + 0) by POLYNOM3:35 ; then A3: S1[ 0 ] ; for j being Element of NAT holds S1[j] from NAT_1:sch_1(A3, A1); hence (p `^ i) *' (p `^ j) = p `^ (i + j) ; ::_thesis: verum end; theorem Th31: :: UPROOTS:31 for L being non empty multLoopStr_0 holds 1_. L = <%(1. L)%> proof let L be non empty multLoopStr_0 ; ::_thesis: 1_. L = <%(1. L)%> A1: dom (0_. L) = NAT by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ (1_._L)_._x_=_<%(1._L)%>_._x let x be set ; ::_thesis: ( x in NAT implies (1_. L) . b1 = <%(1. L)%> . b1 ) assume x in NAT ; ::_thesis: (1_. L) . b1 = <%(1. L)%> . b1 then reconsider n = x as Element of NAT ; percases ( x = 0 or n <> 0 ) ; supposeA2: x = 0 ; ::_thesis: (1_. L) . b1 = <%(1. L)%> . b1 hence (1_. L) . x = 1. L by A1, FUNCT_7:31 .= <%(1. L)%> . x by A2, ALGSEQ_1:def_5 ; ::_thesis: verum end; supposeA3: n <> 0 ; ::_thesis: (1_. L) . b1 = <%(1. L)%> . b1 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 ; ::_thesis: verum end; end; end; hence 1_. L = <%(1. L)%> by FUNCT_2:12; ::_thesis: verum end; theorem :: UPROOTS:32 for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr for p being Polynomial of L holds p *' <%(1. L)%> = p proof let L be non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p *' <%(1. L)%> = p let p be Polynomial of L; ::_thesis: p *' <%(1. L)%> = p thus p *' <%(1. L)%> = p *' (1_. L) by Th31 .= p by POLYNOM3:35 ; ::_thesis: verum end; theorem Th33: :: UPROOTS:33 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds len (p *' q) = 0 proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds len (p *' q) = 0 let p, q be Polynomial of L; ::_thesis: ( ( len p = 0 or len q = 0 ) implies len (p *' q) = 0 ) assume A1: ( len p = 0 or len q = 0 ) ; ::_thesis: len (p *' q) = 0 percases ( len p = 0 or len q = 0 ) by A1; suppose len p = 0 ; ::_thesis: len (p *' q) = 0 then p = 0_. L by POLYNOM4:5; then p *' q = 0_. L by POLYNOM4:2; hence len (p *' q) = 0 by POLYNOM4:3; ::_thesis: verum end; suppose len q = 0 ; ::_thesis: len (p *' q) = 0 then q = 0_. L by POLYNOM4:5; then p *' q = 0_. L by Th20; hence len (p *' q) = 0 by POLYNOM4:3; ::_thesis: verum end; end; end; theorem Th34: :: UPROOTS:34 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for 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 non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st p *' q is non-zero holds ( p is non-zero & q is non-zero ) let p, q be Polynomial of L; ::_thesis: ( p *' q is non-zero implies ( p is non-zero & q is non-zero ) ) assume that A1: p *' q is non-zero and A2: ( not p is non-zero or not q is non-zero ) ; ::_thesis: contradiction ( len p = 0 or len q = 0 ) by A2, Th17; then len (p *' q) = 0 by Th33; hence contradiction by A1, Th17; ::_thesis: verum end; theorem :: UPROOTS:35 for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for 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 non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds 0 < len (p *' q) let p, q be Polynomial of L; ::_thesis: ( (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L implies 0 < len (p *' q) ) assume A1: (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L ; ::_thesis: 0 < len (p *' q) now__::_thesis:_not_len_q_<=_0 assume len q <= 0 ; ::_thesis: contradiction 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; ::_thesis: verum end; then A2: 0 + 1 <= len q by NAT_1:13; now__::_thesis:_not_len_p_<=_0 assume len p <= 0 ; ::_thesis: contradiction 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; ::_thesis: verum end; then 0 + 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 0 < len (p *' q) by A1, POLYNOM4:10; ::_thesis: verum end; theorem Th36: :: UPROOTS:36 for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being Polynomial of L st 1 < len p & 1 < len q holds len p < len (p *' q) proof let L be non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st 1 < len p & 1 < len q holds len p < len (p *' q) let p, q be Polynomial of L; ::_thesis: ( 1 < len p & 1 < len q implies len p < len (p *' q) ) assume that A1: 1 < len p and A2: 1 < len q ; ::_thesis: len p < len (p *' 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 + (len p) by XREAL_1:8; hence len p < len (p *' q) by A3; ::_thesis: verum end; theorem Th37: :: UPROOTS:37 for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr for a, b being Element of L for 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 non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of L for 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)) ) ) let a, b be Element of L; ::_thesis: for 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)) ) ) let q be Polynomial of L; ::_thesis: ( (<%a,b%> *' q) . 0 = a * (q . 0) & ( for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) ) ) set p = <%a,b%>; consider r being FinSequence of L such that A1: len r = 0 + 1 and A2: (<%a,b%> *' q) . 0 = Sum r and A3: for k being Element of NAT st k in dom r holds r . k = (<%a,b%> . (k -' 1)) * (q . ((0 + 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 .= (<%a,b%> . (1 -' 1)) * (q . ((0 + 1) -' 1)) by A3, A4 .= (<%a,b%> . 0) * (q . ((0 + 1) -' 1)) by XREAL_1:232 .= (<%a,b%> . 0) * (q . 0) by NAT_D:34 ; hence (<%a,b%> *' q) . 0 = a * (q . 0) by A2, POLYNOM5:38; ::_thesis: for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) let i be Nat; ::_thesis: (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) consider r being FinSequence of L such that A5: len r = (i + 1) + 1 and A6: (<%a,b%> *' q) . (i + 1) = Sum r and A7: for k being Element of NAT st k in dom r holds r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by POLYNOM3:def_9; len r = i + 2 by A5; then A8: 0 + 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 .= (<%a,b%> . ((1 + 1) -' 1)) * (q . (((i + 1) + 1) -' 2)) by A7, A9 .= (<%a,b%> . 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__::_thesis:_for_k_being_Element_of_NAT_st_2_<_k_&_k_in_dom_r_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( 2 < k & k in dom r implies r . k = 0. L ) assume that A12: 2 < k and A13: k in dom r ; ::_thesis: r . k = 0. L 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 = k1 as Element of NAT by ORDINAL1:def_12; thus r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by A7, A13 .= (<%a,b%> . 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 ; ::_thesis: verum 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 .= (<%a,b%> . (1 -' 1)) * (q . (((i + 1) + 1) -' 1)) by A7, A16 .= (<%a,b%> . 0) * (q . (((i + 1) + 1) -' 1)) by XREAL_1:232 .= (<%a,b%> . 0) * (q . (i + 1)) by NAT_D:34 .= a * (q . (i + 1)) by POLYNOM5:38 ; hence (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) by A6, A8, A10, A11, Th2; ::_thesis: verum end; theorem Th38: :: UPROOTS:38 for L being non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for r being Element of L for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1 proof let L be non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for r being Element of L for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1 let r be Element of L; ::_thesis: for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1 let q be non-zero Polynomial of L; ::_thesis: len (<%r,(1. L)%> *' q) = (len q) + 1 set p = <%r,(1. L)%>; A1: (<%r,(1. L)%> . ((len <%r,(1. L)%>) -' 1)) * (q . ((len q) -' 1)) = (<%r,(1. L)%> . ((1 + 1) -' 1)) * (q . ((len q) -' 1)) by POLYNOM5:40 .= (<%r,(1. L)%> . 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 ; ::_thesis: verum end; theorem Th39: :: UPROOTS:39 for L being non degenerated comRing for x being Element of L for i being Element of NAT holds len (<%x,(1. L)%> `^ i) = i + 1 proof let L be non degenerated comRing; ::_thesis: for x being Element of L for i being Element of NAT holds len (<%x,(1. L)%> `^ i) = i + 1 let x be Element of L; ::_thesis: for i being Element of NAT holds len (<%x,(1. L)%> `^ i) = i + 1 defpred S1[ Element of NAT ] means len (<%x,(1. L)%> `^ $1) = $1 + 1; set r = <%x,(1. L)%>; A1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: S1[i] ; ::_thesis: S1[i + 1] reconsider ri = <%x,(1. L)%> `^ i as non-zero Polynomial of L by A2, Th17; thus len (<%x,(1. L)%> `^ (i + 1)) = len ((<%x,(1. L)%> `^ 1) *' ri) by Th30 .= len (<%x,(1. L)%> *' ri) by POLYNOM5:16 .= (i + 1) + 1 by A2, Th38 ; ::_thesis: verum end; <%x,(1. L)%> `^ 0 = 1_. L by POLYNOM5:15; then A3: S1[ 0 ] by POLYNOM4:4; thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; registration let L be non degenerated comRing; let x be Element of L; let n be Element of NAT ; cluster<%x,(1. L)%> `^ n -> non-zero ; correctness coherence <%x,(1. L)%> `^ n is non-zero ; proof len (<%x,(1. L)%> `^ n) = n + 1 by Th39; hence <%x,(1. L)%> `^ n is non-zero by Th17; ::_thesis: verum end; end; theorem Th40: :: UPROOTS:40 for L being non degenerated comRing for x being Element of L for q being non-zero Polynomial of L for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q) proof let L be non degenerated comRing; ::_thesis: for x being Element of L for q being non-zero Polynomial of L for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q) let x be Element of L; ::_thesis: for q being non-zero Polynomial of L for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q) let q be non-zero Polynomial of L; ::_thesis: for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q) set r = <%x,(1. L)%>; defpred S1[ Element of NAT ] means len ((<%x,(1. L)%> `^ $1) *' q) = $1 + (len q); A1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: S1[i] ; ::_thesis: S1[i + 1] len q > 0 by Th17; then A3: (<%x,(1. L)%> `^ i) *' q is non-zero by A2, Th17; thus len ((<%x,(1. L)%> `^ (i + 1)) *' q) = len (((<%x,(1. L)%> `^ 1) *' (<%x,(1. L)%> `^ i)) *' q) by Th30 .= len ((<%x,(1. L)%> *' (<%x,(1. L)%> `^ i)) *' q) by POLYNOM5:16 .= len (<%x,(1. L)%> *' ((<%x,(1. L)%> `^ i) *' q)) by POLYNOM3:33 .= (i + (len q)) + 1 by A2, A3, Th38 .= (i + 1) + (len q) ; ::_thesis: verum end; len ((<%x,(1. L)%> `^ 0) *' q) = len ((1_. L) *' q) by POLYNOM5:15 .= 0 + (len q) by POLYNOM3:35 ; then A4: S1[ 0 ] ; thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A4, A1); ::_thesis: verum end; theorem Th41: :: UPROOTS:41 for L being non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for r being Element of L for 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 non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for r being Element of L for 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 let x be Element of L; ::_thesis: for p, q being Polynomial of L st p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds q . ((len q) -' 1) = 1. L let p, q be Polynomial of L; ::_thesis: ( p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L implies q . ((len q) -' 1) = 1. L ) assume that A1: p = <%x,(1. L)%> *' q and A2: p . ((len p) -' 1) = 1. L ; ::_thesis: q . ((len q) -' 1) = 1. L set lp1 = (len p) -' 1; A3: now__::_thesis:_not_q_=_0_._L assume q = 0_. L ; ::_thesis: contradiction then p = 0_. L by A1, POLYNOM3:34; hence contradiction by A2, FUNCOP_1:7; ::_thesis: verum end; then q is non-zero by Def5; then len p = (len q) + 1 by A1, Th38; then A4: (len p) -' 1 = len q by NAT_D:34; then consider lp2 being Nat such that A5: (len p) -' 1 = lp2 + 1 by A3, NAT_1:6, POLYNOM4:5; reconsider lp2 = lp2 as Element of NAT by ORDINAL1:def_12; A6: q . ((len p) -' 1) = 0. L by A4, ALGSEQ_1:8; (<%x,(1. L)%> *' q) . ((len p) -' 1) = (x * (q . ((len p) -' 1))) + ((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 q . ((len q) -' 1) = 1. L by A1, A2, A4, A5, NAT_D:34; ::_thesis: verum end; begin definition let L be non empty ZeroStr ; let p be Polynomial of L; let n be Nat; func poly_shift (p,n) -> Polynomial of L means :Def6: :: UPROOTS:def 6 for i being Nat holds it . i = p . (n + i); existence ex b1 being Polynomial of L st for i being Nat holds b1 . i = p . (n + i) proof deffunc H1( Nat) -> Element of the carrier of L = 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 = H1(k) from ALGSEQ_1:sch_1(); take ps ; ::_thesis: for i being Nat holds ps . i = p . (n + i) let i be Nat; ::_thesis: ps . i = p . (n + i) percases ( i < len p or i >= len p ) ; suppose i < len p ; ::_thesis: ps . i = p . (n + i) hence ps . i = p . (n + i) by A2; ::_thesis: verum end; supposeA3: i >= len p ; ::_thesis: ps . i = p . (n + i) hence ps . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2 .= p . (n + i) by A3, ALGSEQ_1:8, NAT_1:12 ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Polynomial of L st ( for i being Nat holds b1 . i = p . (n + i) ) & ( for i being Nat holds b2 . i = p . (n + i) ) holds b1 = b2 proof let it1, it2 be Polynomial of L; ::_thesis: ( ( for i being Nat holds it1 . i = p . (n + i) ) & ( for i being Nat holds it2 . i = p . (n + i) ) implies it1 = it2 ) assume that A4: for i being Nat holds it1 . i = p . (n + i) and A5: for i being Nat holds it2 . i = p . (n + i) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ it1_._x_=_it2_._x let x be set ; ::_thesis: ( x in NAT implies it1 . x = it2 . x ) assume x in NAT ; ::_thesis: it1 . x = it2 . x then reconsider i = x as Element of NAT ; thus it1 . x = p . (n + i) by A4 .= it2 . x by A5 ; ::_thesis: verum end; hence it1 = it2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def6 defines poly_shift UPROOTS:def_6_:_ for L being non empty ZeroStr for p being Polynomial of L for n being Nat for b4 being Polynomial of L holds ( b4 = poly_shift (p,n) iff for i being Nat holds b4 . i = p . (n + i) ); theorem Th42: :: UPROOTS:42 for L being non empty ZeroStr for p being Polynomial of L holds poly_shift (p,0) = p proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L holds poly_shift (p,0) = p let p be Polynomial of L; ::_thesis: poly_shift (p,0) = p set ps = poly_shift (p,0); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ (poly_shift_(p,0))_._x_=_p_._x let x be set ; ::_thesis: ( x in NAT implies (poly_shift (p,0)) . x = p . x ) assume x in NAT ; ::_thesis: (poly_shift (p,0)) . x = p . x then reconsider i = x as Element of NAT ; thus (poly_shift (p,0)) . x = p . (0 + i) by Def6 .= p . x ; ::_thesis: verum end; hence poly_shift (p,0) = p by FUNCT_2:12; ::_thesis: verum end; theorem Th43: :: UPROOTS:43 for L being non empty ZeroStr for n being Element of NAT for p being Polynomial of L st n >= len p holds poly_shift (p,n) = 0_. L proof let L be non empty ZeroStr ; ::_thesis: for n being Element of NAT for p being Polynomial of L st n >= len p holds poly_shift (p,n) = 0_. L let n be Element of NAT ; ::_thesis: for p being Polynomial of L st n >= len p holds poly_shift (p,n) = 0_. L let p be Polynomial of L; ::_thesis: ( n >= len p implies poly_shift (p,n) = 0_. L ) set ps = poly_shift (p,n); assume A1: n >= len p ; ::_thesis: poly_shift (p,n) = 0_. L A2: now__::_thesis:_for_z_being_set_st_z_in_dom_(poly_shift_(p,n))_holds_ (poly_shift_(p,n))_._z_=_0._L let z be set ; ::_thesis: ( z in dom (poly_shift (p,n)) implies (poly_shift (p,n)) . z = 0. L ) assume z in dom (poly_shift (p,n)) ; ::_thesis: (poly_shift (p,n)) . z = 0. L then reconsider i = z as Element of NAT ; thus (poly_shift (p,n)) . z = p . (n + i) by Def6 .= 0. L by A1, ALGSEQ_1:8, NAT_1:12 ; ::_thesis: verum end; dom (poly_shift (p,n)) = NAT by FUNCT_2:def_1; hence poly_shift (p,n) = 0_. L by A2, FUNCOP_1:11; ::_thesis: verum end; theorem Th44: :: UPROOTS:44 for L being non empty non degenerated multLoopStr_0 for n being Element of NAT for p being Polynomial of L st n <= len p holds (len (poly_shift (p,n))) + n = len p proof let L be non empty non degenerated multLoopStr_0 ; ::_thesis: for n being Element of NAT for p being Polynomial of L st n <= len p holds (len (poly_shift (p,n))) + n = len p let n be Element of NAT ; ::_thesis: for p being Polynomial of L st n <= len p holds (len (poly_shift (p,n))) + n = len p let p be Polynomial of L; ::_thesis: ( n <= len p implies (len (poly_shift (p,n))) + n = len p ) assume A1: n <= len p ; ::_thesis: (len (poly_shift (p,n))) + n = len p set ps = poly_shift (p,n); set lpn = (len p) - n; n - n <= (len p) - n by A1, XREAL_1:9; then reconsider lpn = (len p) - n as Element of NAT by INT_1:3; A2: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_poly_shift_(p,n)_holds_ not_lpn_>_m let m be Nat; ::_thesis: ( m is_at_least_length_of poly_shift (p,n) implies not lpn > m ) assume that A3: m is_at_least_length_of poly_shift (p,n) and A4: lpn > m ; ::_thesis: contradiction 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; (poly_shift (p,n)) . lpn1 = p . (n + lpn1) by Def6; hence contradiction by A3, A5, A6, ALGSEQ_1:def_2; ::_thesis: verum end; now__::_thesis:_for_i_being_Nat_st_i_>=_lpn_holds_ (poly_shift_(p,n))_._i_=_0._L let i be Nat; ::_thesis: ( i >= lpn implies (poly_shift (p,n)) . i = 0. L ) assume i >= lpn ; ::_thesis: (poly_shift (p,n)) . i = 0. L then A7: i + n >= len p by XREAL_1:20; thus (poly_shift (p,n)) . i = p . (n + i) by Def6 .= 0. L by A7, ALGSEQ_1:8 ; ::_thesis: verum end; then lpn is_at_least_length_of poly_shift (p,n) by ALGSEQ_1:def_2; hence (len (poly_shift (p,n))) + n = lpn + n by A2, ALGSEQ_1:def_3 .= len p ; ::_thesis: verum end; theorem Th45: :: UPROOTS:45 for L being non degenerated comRing for x being Element of L for n being Element of NAT for 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; ::_thesis: for x being Element of L for n being Element of NAT for 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) let x be Element of L; ::_thesis: for n being Element of NAT for 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) let n be Element of NAT ; ::_thesis: for 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) let p be Polynomial of L; ::_thesis: ( n < len p implies eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) ) assume A1: n < len p ; ::_thesis: eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) set ps = poly_shift (p,n); set ps1 = poly_shift (p,(n + 1)); consider f being FinSequence of L such that A2: eval ((poly_shift (p,n)),x) = Sum f and A3: len f = len (poly_shift (p,n)) and A4: for k being Element of NAT st k in dom f holds f . k = ((poly_shift (p,n)) . (k -' 1)) * ((power L) . (x,(k -' 1))) by POLYNOM4:def_2; consider f1 being FinSequence of L such that A5: eval ((poly_shift (p,(n + 1))),x) = Sum f1 and A6: len f1 = len (poly_shift (p,(n + 1))) and A7: for k being Element of NAT st k in dom f1 holds f1 . k = ((poly_shift (p,(n + 1))) . (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__::_thesis:_(_len_f_=_len_f_&_len_(<*(p_._n)*>_^_(x_*_f1))_=_len_f_&_(_for_j_being_Nat_st_j_in_dom_f_holds_ f_._j_=_(<*(p_._n)*>_^_(x_*_f1))_._j_)_) A10: n + 1 <= len p by A1, NAT_1:13; A11: ((len (poly_shift (p,(n + 1)))) + 1) + n = (len (poly_shift (p,(n + 1)))) + (n + 1) .= len p by A10, Th44 .= (len (poly_shift (p,n))) + n by A1, Th44 ; thus len f = len f ; ::_thesis: ( len (<*(p . n)*> ^ (x * f1)) = len f & ( for j being Nat st j in dom f holds f . b2 = (<*(p . n)*> ^ (x * f1)) . b2 ) ) 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; ::_thesis: for j being Nat st j in dom f holds f . b2 = (<*(p . n)*> ^ (x * f1)) . b2 let j be Nat; ::_thesis: ( j in dom f implies f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 ) assume A14: j in dom f ; ::_thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 A15: 1 <= j by A14, FINSEQ_3:25; A16: j <= len f by A14, FINSEQ_3:25; percases ( j = 1 or 1 < j ) by A15, XXREAL_0:1; supposeA17: j = 1 ; ::_thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 A18: 1 in dom <*(p . n)*> by A12, FINSEQ_3:25; thus f . j = ((poly_shift (p,n)) . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A4, A14, A17 .= ((poly_shift (p,n)) . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232 .= ((poly_shift (p,n)) . 0) * ((power L) . (x,0)) by XREAL_1:232 .= ((poly_shift (p,n)) . 0) * (1. L) by A9, GROUP_1:def_7 .= (poly_shift (p,n)) . 0 by A9, GROUP_1:def_4 .= p . (n + 0) by Def6 .= <*(p . n)*> . 1 by FINSEQ_1:40 .= (<*(p . n)*> ^ (x * f1)) . j by A17, A18, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA19: 1 < j ; ::_thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 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 = ((poly_shift (p,n)) . (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 * (((poly_shift (p,(n + 1))) . (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 ; ::_thesis: verum end; end; end; then ( x * (Sum f1) = Sum (x * f1) & f = <*(p . n)*> ^ (x * f1) ) by FINSEQ_2:9, FVSUM_1:73; hence eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) by A2, A5, FVSUM_1:72; ::_thesis: verum end; theorem Th46: :: UPROOTS:46 for L being non degenerated comRing for p being Polynomial of L st len p = 1 holds Roots p = {} proof let L be non degenerated comRing; ::_thesis: for p being Polynomial of L st len p = 1 holds Roots p = {} let p be Polynomial of L; ::_thesis: ( len p = 1 implies Roots p = {} ) assume len p = 1 ; ::_thesis: Roots p = {} then A1: ( p = <%(p . 0)%> & p . 0 <> 0. L ) by Th19; assume Roots p <> {} ; ::_thesis: contradiction then consider x being set such that A2: x in Roots p by XBOOLE_0:def_1; reconsider x = 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; ::_thesis: verum end; definition let L be non degenerated comRing; let r be Element of L; let p be Polynomial of L; assume A1: r is_a_root_of p ; func poly_quotient (p,r) -> Polynomial of L means :Def7: :: UPROOTS:def 7 ( (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 ( ( len p > 0 implies ex b1 being Polynomial of L st ( (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) & ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) ) proof hereby ::_thesis: ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) r in Roots p by A1, POLYNOM5:def_9; then A1: len p <> 1 by Th46; deffunc H1( Nat) -> Element of the carrier of L = 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 = H1(k) from FUNCT_2:sch_4(); reconsider q = q as sequence of L ; assume A3: len p > 0 ; ::_thesis: ex q being AlgSequence of L st ( (len q) + 1 = len p & ( for k being Nat holds q . k = H1(k) ) ) then consider p1 being Nat such that A4: len p = p1 + 1 by NAT_1:6; A5: (len p) -' 1 = p1 by A4, NAT_D:34; then A6: (len p) -' 1 < len p by A4, NAT_1:13; len p >= 0 + 1 by A3, NAT_1:13; then consider lq1 being Nat such that A7: (len p) -' 1 = lq1 + 1 by A4, A5, A1, NAT_1:6; A8: now__::_thesis:_for_i_being_Nat_st_i_>=_(len_p)_-'_1_holds_ q_._i_=_0._L let i be Nat; ::_thesis: ( i >= (len p) -' 1 implies q . i = 0. L ) assume i >= (len p) -' 1 ; ::_thesis: q . i = 0. L 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 ; ::_thesis: verum end; reconsider lq1 = 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 . ((len p) -' 1)) by A4, A5, A7, A6, Th45 .= (r * (eval ((0_. L),r))) + (p . ((len p) -' 1)) by Th43 .= (r * (0. L)) + (p . ((len p) -' 1)) by POLYNOM4:17 .= (0. L) + (p . ((len p) -' 1)) by VECTSP_1:6 .= p . ((len p) -' 1) by RLVECT_1:4 ; then A10: q . lq1 <> 0. L by A4, A5, ALGSEQ_1:10; reconsider q = q as AlgSequence of L by A8, ALGSEQ_1:def_1; A11: lq1 = ((len p) -' 1) -' 1 by A7, NAT_D:34; A12: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_q_holds_ not_(len_p)_-'_1_>_m let m be Nat; ::_thesis: ( m is_at_least_length_of q implies not (len p) -' 1 > m ) assume A13: m is_at_least_length_of q ; ::_thesis: not (len p) -' 1 > m assume A14: (len p) -' 1 > m ; ::_thesis: contradiction then consider lq1 being Nat such that A15: (len p) -' 1 = lq1 + 1 by NAT_1:6; lq1 >= m by A14, A15, NAT_1:13; then ((len p) -' 1) -' 1 >= m by A15, NAT_D:34; hence contradiction by A11, A10, A13, ALGSEQ_1:def_2; ::_thesis: verum end; take q = q; ::_thesis: ( (len q) + 1 = len p & ( for k being Nat holds q . k = H1(k) ) ) (len p) -' 1 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 ; ::_thesis: for k being Nat holds q . k = H1(k) let k be Nat; ::_thesis: q . k = H1(k) k in NAT by ORDINAL1:def_12; hence q . k = H1(k) by A2; ::_thesis: verum end; thus ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) ; ::_thesis: verum end; uniqueness for b1, b2 being Polynomial of L holds ( ( len p > 0 & (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len b2) + 1 = len p & ( for i being Nat holds b2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies b1 = b2 ) & ( not len p > 0 & b1 = 0_. L & b2 = 0_. L implies b1 = b2 ) ) proof let it1, it2 be Polynomial of L; ::_thesis: ( ( len p > 0 & (len it1) + 1 = len p & ( for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len it2) + 1 = len p & ( for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies it1 = it2 ) & ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 ) ) hereby ::_thesis: ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 ) assume len p > 0 ; ::_thesis: ( (len it1) + 1 = len p & ( for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len it2) + 1 = len p & ( for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies it1 = it2 ) 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) ; ::_thesis: it1 = it2 now__::_thesis:_for_k_being_Nat_st_k_<_len_it1_holds_ it1_._k_=_it2_._k let k be Nat; ::_thesis: ( k < len it1 implies it1 . k = it2 . k ) assume k < len it1 ; ::_thesis: it1 . k = it2 . k thus it1 . k = eval ((poly_shift (p,(k + 1))),r) by A17 .= it2 . k by A19 ; ::_thesis: verum end; hence it1 = it2 by A16, A18, ALGSEQ_1:12; ::_thesis: verum end; thus ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 ) ; ::_thesis: verum end; consistency for b1 being Polynomial of L holds verum ; end; :: deftheorem Def7 defines poly_quotient UPROOTS:def_7_:_ for L being non degenerated comRing for r being Element of L for p being Polynomial of L st r is_a_root_of p holds for b4 being Polynomial of L holds ( ( len p > 0 implies ( b4 = poly_quotient (p,r) iff ( (len b4) + 1 = len p & ( for i being Nat holds b4 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) ) & ( not len p > 0 implies ( b4 = poly_quotient (p,r) iff b4 = 0_. L ) ) ); theorem Th47: :: UPROOTS:47 for L being non degenerated comRing for r being Element of L for 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; ::_thesis: for r being Element of L for p being non-zero Polynomial of L st r is_a_root_of p holds len (poly_quotient (p,r)) > 0 let r be Element of L; ::_thesis: for p being non-zero Polynomial of L st r is_a_root_of p holds len (poly_quotient (p,r)) > 0 let p be non-zero Polynomial of L; ::_thesis: ( r is_a_root_of p implies len (poly_quotient (p,r)) > 0 ) assume A1: r is_a_root_of p ; ::_thesis: len (poly_quotient (p,r)) > 0 assume len (poly_quotient (p,r)) <= 0 ; ::_thesis: contradiction 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; ::_thesis: verum end; theorem Th48: :: UPROOTS:48 for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr for x being Element of L holds Roots <%(- x),(1. L)%> = {x} proof let L be non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for x being Element of L holds Roots <%(- x),(1. L)%> = {x} let x be Element of L; ::_thesis: Roots <%(- x),(1. L)%> = {x} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_Roots_<%(-_x),(1._L)%>_implies_x_=_a_)_&_(_a_=_x_implies_a_in_Roots_<%(-_x),(1._L)%>_)_) let a be set ; ::_thesis: ( ( a in Roots <%(- x),(1. L)%> implies x = a ) & ( a = x implies a in Roots <%(- x),(1. L)%> ) ) hereby ::_thesis: ( a = x implies a in Roots <%(- x),(1. L)%> ) assume A1: a in Roots <%(- x),(1. L)%> ; ::_thesis: x = a 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; ::_thesis: verum 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 ; ::_thesis: a in Roots <%(- x),(1. L)%> hence a in Roots <%(- x),(1. L)%> by A2, POLYNOM5:def_9; ::_thesis: verum end; hence Roots <%(- x),(1. L)%> = {x} by TARSKI:def_1; ::_thesis: verum end; theorem Th49: :: UPROOTS:49 for L being non trivial comRing for x being Element of L for 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; ::_thesis: for x being Element of L for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds x is_a_root_of p let x be Element of L; ::_thesis: for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds x is_a_root_of p let p, q be Polynomial of L; ::_thesis: ( p = <%(- x),(1. L)%> *' q implies x is_a_root_of p ) assume A1: p = <%(- x),(1. L)%> *' q ; ::_thesis: x is_a_root_of p 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 ; :: according to POLYNOM5:def_6 ::_thesis: verum end; theorem Th50: :: UPROOTS:50 for L being non degenerated comRing for r being Element of L for 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; ::_thesis: for r being Element of L for p being Polynomial of L st r is_a_root_of p holds p = <%(- r),(1. L)%> *' (poly_quotient (p,r)) let x be Element of L; ::_thesis: for p being Polynomial of L st x is_a_root_of p holds p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) let p be Polynomial of L; ::_thesis: ( x is_a_root_of p implies p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) ) assume A1: x is_a_root_of p ; ::_thesis: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) set r = <%(- x),(1. L)%>; set pq = poly_quotient (p,x); percases ( len p > 0 or len p = 0 ) ; supposeA2: len p > 0 ; ::_thesis: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) <%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) = <%(- x),(1. L)%> . ((1 + 1) -' 1) by POLYNOM5:40 .= <%(- x),(1. L)%> . 1 by NAT_D:34 .= 1. L by POLYNOM5:38 ; then A3: (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1)) * ((poly_quotient (p,x)) . ((len (poly_quotient (p,x))) -' 1)) = (poly_quotient (p,x)) . ((len (poly_quotient (p,x))) -' 1) by VECTSP_1:def_8; p is non-zero by A2, Th17; then A4: len (poly_quotient (p,x)) > 0 by A1, Th47; now__::_thesis:_(_len_p_=_len_(<%(-_x),(1._L)%>_*'_(poly_quotient_(p,x)))_&_(_for_k_being_Nat_st_k_<_len_p_holds_ p_._k_=_(<%(-_x),(1._L)%>_*'_(poly_quotient_(p,x)))_._k_)_) len (<%(- x),(1. L)%> *' (poly_quotient (p,x))) = ((len <%(- x),(1. L)%>) + (len (poly_quotient (p,x)))) - 1 by A4, A3, Th18, POLYNOM4:10 .= ((len (poly_quotient (p,x))) + (1 + 1)) - 1 by POLYNOM5:40 .= (len (poly_quotient (p,x))) + 1 .= len p by A1, A2, Def7 ; hence len p = len (<%(- x),(1. L)%> *' (poly_quotient (p,x))) ; ::_thesis: for k being Nat st k < len p holds p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k defpred S1[ Nat] means p . $1 = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . $1; let k be Nat; ::_thesis: ( k < len p implies p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k ) assume k < len p ; ::_thesis: p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k 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 + 1))),x))) + (p . 0) by A2, Th45 ; A6: (- x) * (eval ((poly_shift (p,(0 + 1))),x)) = ((- x) * (eval ((poly_shift (p,(0 + 1))),x))) + (0. L) by RLVECT_1:def_4 .= (((- x) * (eval ((poly_shift (p,(0 + 1))),x))) + (x * (eval ((poly_shift (p,1)),x)))) + (p . 0) by A5, RLVECT_1:def_3 .= ((- (x * (eval ((poly_shift (p,(0 + 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 S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] A8: (poly_quotient (p,x)) . (k + 1) = eval ((poly_shift (p,((k + 1) + 1))),x) by A1, A2, Def7; A9: (poly_quotient (p,x)) . k = eval ((poly_shift (p,(k + 1))),x) by A1, A2, Def7; percases ( k + 1 >= len p or k + 1 < len p ) ; supposeA10: k + 1 >= len p ; ::_thesis: S1[k + 1] then A11: (poly_quotient (p,x)) . (k + 1) = eval ((0_. L),x) by A8, Th43, NAT_1:12 .= 0. L by POLYNOM4:17 ; A12: (poly_quotient (p,x)) . k = eval ((0_. L),x) by A9, A10, Th43 .= 0. L by POLYNOM4:17 ; (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . (k + 1) = ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((1. L) * ((poly_quotient (p,x)) . k)) by Th37 .= (0. L) + ((1. L) * ((poly_quotient (p,x)) . k)) by A11, VECTSP_1:6 .= (0. L) + (0. L) by A12, VECTSP_1:6 .= 0. L by RLVECT_1:4 ; hence S1[k + 1] by A10, ALGSEQ_1:8; ::_thesis: verum end; suppose k + 1 < len p ; ::_thesis: S1[k + 1] then (poly_quotient (p,x)) . k = (x * (eval ((poly_shift (p,((k + 1) + 1))),x))) + (p . (k + 1)) by A9, Th45; then A13: (- (x * ((poly_quotient (p,x)) . (k + 1)))) + ((poly_quotient (p,x)) . k) = ((- (x * ((poly_quotient (p,x)) . (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 ; (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . (k + 1) = ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((1. L) * ((poly_quotient (p,x)) . k)) by Th37 .= ((- x) * ((poly_quotient (p,x)) . (k + 1))) + ((poly_quotient (p,x)) . k) by VECTSP_1:def_8 .= (- (x * ((poly_quotient (p,x)) . (k + 1)))) + ((poly_quotient (p,x)) . k) by VECTSP_1:9 ; hence S1[k + 1] by A13, RLVECT_1:4; ::_thesis: verum end; end; end; (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . 0 = (- x) * ((poly_quotient (p,x)) . 0) by Th37 .= (- x) * (eval ((poly_shift (p,(0 + 1))),x)) by A1, A2, Def7 ; then A14: S1[ 0 ] by A6; for k being Nat holds S1[k] from NAT_1:sch_2(A14, A7); hence p . k = (<%(- x),(1. L)%> *' (poly_quotient (p,x))) . k ; ::_thesis: verum end; hence p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by ALGSEQ_1:12; ::_thesis: verum end; suppose len p = 0 ; ::_thesis: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) then ( poly_quotient (p,x) = 0_. L & p = 0_. L ) by A1, Def7, POLYNOM4:5; hence p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by POLYNOM3:34; ::_thesis: verum end; end; end; theorem :: UPROOTS:51 for L being non degenerated comRing for r being Element of L for 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; ::_thesis: for r being Element of L for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds r is_a_root_of p let r be Element of L; ::_thesis: for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds r is_a_root_of p let p, q be Polynomial of L; ::_thesis: ( p = <%(- r),(1. L)%> *' q implies r is_a_root_of p ) assume p = <%(- r),(1. L)%> *' q ; ::_thesis: r is_a_root_of p 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 r is_a_root_of p by POLYNOM5:def_6; ::_thesis: verum end; Lm1: now__::_thesis:_for_L_being_domRing for_p_being_non-zero_Polynomial_of_L_holds_ (_Roots_p_is_finite_&_ex_n_being_Element_of_NAT_st_ (_n_=_card_(Roots_p)_&_n_<_len_p_)_) let L be domRing; ::_thesis: for p being non-zero Polynomial of L holds ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) let p be non-zero Polynomial of L; ::_thesis: ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) defpred S1[ 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 + 1 by NAT_1:13; A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that n >= 1 and A3: S1[n] ; ::_thesis: S1[n + 1] let p be Polynomial of L; ::_thesis: ( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) ) assume A4: len p = n + 1 ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) percases ( p is with_roots or not p is with_roots ) ; suppose p is with_roots ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) 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)%>; set pq = poly_quotient (p,x); A6: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A5, Th50; then A7: Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x))) by Th23; A8: Roots <%(- x),(1. L)%> = {x} by Th48; then reconsider Rr = Roots <%(- x),(1. L)%> as finite set ; A9: (len (poly_quotient (p,x))) + 1 = len p by A4, A5, Def7; then consider k being Element of NAT such that A10: k = card (Roots (poly_quotient (p,x))) and A11: k < len (poly_quotient (p,x)) by A3, A4; reconsider Rpq = Roots (poly_quotient (p,x)) 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 (poly_quotient (p,x)) is finite by A3, A4, A9; hence Roots p is finite by A8, A7; ::_thesis: ex n being Element of NAT st ( n = card (Roots p) & n < len p ) take m = card Rp; ::_thesis: ( m = card (Roots p) & m < len p ) thus m = card (Roots p) by A6, Th23; ::_thesis: m < len p k + 1 < n + 1 by A4, A9, A11, XREAL_1:8; hence m < len p by A4, A12, XXREAL_0:2; ::_thesis: verum end; supposeA13: not p is with_roots ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) A14: now__::_thesis:_not_Roots_p_<>_{} assume Roots p <> {} ; ::_thesis: contradiction then consider x being set such that A15: x in Roots p by XBOOLE_0:def_1; reconsider x = 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; ::_thesis: verum end; hence Roots p is finite ; ::_thesis: ex n being Element of NAT st ( n = card (Roots p) & n < len p ) take 0 ; ::_thesis: ( 0 = card (Roots p) & 0 < len p ) thus 0 = card (Roots p) by A14; ::_thesis: 0 < len p thus 0 < len p by A4; ::_thesis: verum end; end; end; A16: S1[1] proof let p be Polynomial of L; ::_thesis: ( len p = 1 implies ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) ) assume A17: len p = 1 ; ::_thesis: ( Roots p is finite & ex n being Element of NAT st ( n = card (Roots p) & n < len p ) ) hence Roots p is finite by Th46; ::_thesis: ex n being Element of NAT st ( n = card (Roots p) & n < len p ) take 0 ; ::_thesis: ( 0 = card (Roots p) & 0 < len p ) thus 0 = card (Roots p) by A17, Th46, CARD_1:27; ::_thesis: 0 < len p thus 0 < len p by A17; ::_thesis: verum end; for n being Nat st n >= 1 holds S1[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; ::_thesis: verum end; begin registration let L be domRing; let p be non-zero Polynomial of L; cluster Roots p -> finite ; correctness coherence Roots p is finite ; by Lm1; end; definition let L be non degenerated comRing; let x be Element of L; let p be non-zero Polynomial of L; func multiplicity (p,x) -> Element of NAT means :Def8: :: UPROOTS:def 8 ex F being non empty finite 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 ex b1 being Element of NAT ex F being non empty finite 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 } & b1 = max F ) proof set r = <%(- x),(1. L)%>; defpred S1[ Element of NAT ] means ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ $1) *' q; set F = { k where k is Element of NAT : S1[k] } ; A1: { k where k is Element of NAT : S1[k] } c= NAT from FRAENKEL:sch_10(); p = (1_. L) *' p by POLYNOM3:35 .= (<%(- x),(1. L)%> `^ 0) *' p by POLYNOM5:15 ; then A2: 0 in { k where k is Element of NAT : S1[k] } ; A3: len p > 0 by Th17; { k where k is Element of NAT : S1[k] } c= len p proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { k where k is Element of NAT : S1[k] } or a in len p ) assume a in { k where k is Element of NAT : S1[k] } ; ::_thesis: a in len p then consider k being Element of NAT such that A4: a = k and A5: S1[k] ; consider q being Polynomial of L such that A6: p = (<%(- x),(1. L)%> `^ k) *' q by A5; A7: now__::_thesis:_not_len_q_=_0 assume len q = 0 ; ::_thesis: contradiction then q = 0_. L by POLYNOM4:5; then p = 0_. L by A6, POLYNOM4:2; hence contradiction by A3, POLYNOM4:3; ::_thesis: verum end; then reconsider q = q as non-zero Polynomial of L by Th17; now__::_thesis:_not_k_>=_len_p assume k >= len p ; ::_thesis: contradiction then k + (len q) > (len p) + 0 by A7, XREAL_1:8; hence contradiction by A6, Th40; ::_thesis: verum end; then k in { i where i is Element of NAT : i < len p } ; hence a in len p by A4, AXIOMS:4; ::_thesis: verum end; then reconsider F = { k where k is Element of NAT : S1[k] } as non empty finite Subset of NAT by A2, A1; reconsider FF = F as non empty finite natural-membered set ; reconsider m = max FF as Element of NAT by ORDINAL1:def_12; take m ; ::_thesis: ex F being non empty finite 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 } & m = max F ) thus ex F being non empty finite 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 } & m = max F ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ex F being non empty finite 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 } & b1 = max F ) & ex F being non empty finite 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 } & b2 = max F ) holds b1 = b2 ; end; :: deftheorem Def8 defines multiplicity UPROOTS:def_8_:_ for L being non degenerated comRing for x being Element of L for p being non-zero Polynomial of L for b4 being Element of NAT holds ( b4 = multiplicity (p,x) iff ex F being non empty finite 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 } & b4 = max F ) ); theorem Th52: :: UPROOTS:52 for L being non degenerated comRing for p being non-zero Polynomial of L for x being Element of L holds ( x is_a_root_of p iff multiplicity (p,x) >= 1 ) proof let L be non degenerated comRing; ::_thesis: for p being non-zero Polynomial of L for x being Element of L holds ( x is_a_root_of p iff multiplicity (p,x) >= 1 ) let p be non-zero Polynomial of L; ::_thesis: for x being Element of L holds ( x is_a_root_of p iff multiplicity (p,x) >= 1 ) let x be Element of L; ::_thesis: ( x is_a_root_of p iff multiplicity (p,x) >= 1 ) set r = <%(- x),(1. L)%>; set m = multiplicity (p,x); consider F being non empty finite Subset of NAT such that A1: F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } and A2: multiplicity (p,x) = max F by Def8; multiplicity (p,x) in F by A2, XXREAL_2:def_8; then consider k being Element of NAT such that A3: multiplicity (p,x) = k and A4: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q by A1; hereby ::_thesis: ( multiplicity (p,x) >= 1 implies x is_a_root_of p ) assume x is_a_root_of p ; ::_thesis: multiplicity (p,x) >= 1 then A5: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by Th50; <%(- x),(1. L)%> `^ 1 = <%(- x),(1. L)%> by POLYNOM5:16; then 1 in F by A1, A5; hence multiplicity (p,x) >= 1 by A2, XXREAL_2:def_8; ::_thesis: verum end; consider q being Polynomial of L such that A6: p = (<%(- x),(1. L)%> `^ k) *' q by A4; assume multiplicity (p,x) >= 1 ; ::_thesis: x is_a_root_of p then consider k1 being Nat such that A7: k = k1 + 1 by A3, NAT_1:6; reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12; p = (<%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ k1)) *' q by A6, A7, POLYNOM5:19 .= <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ k1) *' q) by POLYNOM3:33 ; hence x is_a_root_of p by Th49; ::_thesis: verum end; theorem Th53: :: UPROOTS:53 for L being non degenerated comRing for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1 proof let L be non degenerated comRing; ::_thesis: for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1 let x be Element of L; ::_thesis: multiplicity (<%(- x),(1. L)%>,x) = 1 set r = <%(- x),(1. L)%>; set j = multiplicity (<%(- x),(1. L)%>,x); consider F being non empty finite Subset of NAT such that A1: F = { k where k is Element of NAT : ex q being Polynomial of L st <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q } and A2: multiplicity (<%(- x),(1. L)%>,x) = max F by Def8; multiplicity (<%(- x),(1. L)%>,x) in F by A2, XXREAL_2:def_8; then consider k being Element of NAT such that A3: k = multiplicity (<%(- x),(1. L)%>,x) and A4: ex q being Polynomial of L st <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A1; consider q being Polynomial of L such that A5: <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A4; A6: len <%(- x),(1. L)%> = 2 by POLYNOM5:40; A7: now__::_thesis:_not_len_q_=_0 assume len q = 0 ; ::_thesis: contradiction then q = 0_. L by POLYNOM4:5; then <%(- x),(1. L)%> = 0_. L by A5, POLYNOM4:2; hence contradiction by A6, POLYNOM4:3; ::_thesis: verum end; then A8: q is non-zero by Th17; A9: now__::_thesis:_not_k_>_1 assume k > 1 ; ::_thesis: contradiction then k >= 1 + 1 by NAT_1:13; then k + (len q) > 2 + 0 by A7, XREAL_1:8; hence contradiction by A6, A5, A8, Th40; ::_thesis: verum end; <%(- x),(1. L)%> = <%(- x),(1. L)%> `^ 1 by POLYNOM5:16; then <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ 1) *' (1_. L) by POLYNOM3:35; then 1 in F by A1; then multiplicity (<%(- x),(1. L)%>,x) >= 1 by A2, XXREAL_2:def_8; hence multiplicity (<%(- x),(1. L)%>,x) = 1 by A3, A9, XXREAL_0:1; ::_thesis: verum end; definition let L be domRing; let p be non-zero Polynomial of L; func BRoots p -> bag of the carrier of L means :Def9: :: UPROOTS:def 9 ( support it = Roots p & ( for x being Element of L holds it . x = multiplicity (p,x) ) ); existence ex b1 being bag of the carrier of L st ( support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity (p,x) ) ) proof deffunc H1( Element of L) -> Element of NAT = 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 = H1(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__::_thesis:_for_x_being_set_holds_ (_(_x_in_support_b_implies_x_in_Roots_p_)_&_(_x_in_Roots_p_implies_x_in_support_b_)_) let x be set ; ::_thesis: ( ( x in support b implies x in Roots p ) & ( x in Roots p implies x in support b ) ) hereby ::_thesis: ( x in Roots p implies x in support b ) assume A4: x in support b ; ::_thesis: x in Roots p then reconsider xx = x as Element of L by A2; b . x <> 0 by A4, PRE_POLY:def_7; then A5: b . xx >= 0 + 1 by NAT_1:13; b . x = H1(xx) by A1; then xx is_a_root_of p by A5, Th52; hence x in Roots p by POLYNOM5:def_9; ::_thesis: verum end; assume A6: x in Roots p ; ::_thesis: x in support b 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; ::_thesis: verum end; then support b = Roots p by TARSKI:1; then reconsider b = b as bag of the carrier of L by PRE_POLY:def_8; take b ; ::_thesis: ( support b = Roots p & ( for x being Element of L holds b . x = multiplicity (p,x) ) ) thus ( support b = Roots p & ( for x being Element of L holds b . x = multiplicity (p,x) ) ) by A1, A3, TARSKI:1; ::_thesis: verum end; uniqueness for b1, b2 being bag of the carrier of L st support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity (p,x) ) & support b2 = Roots p & ( for x being Element of L holds b2 . x = multiplicity (p,x) ) holds b1 = b2 proof let it1, it2 be bag of the carrier of L; ::_thesis: ( support it1 = Roots p & ( for x being Element of L holds it1 . x = multiplicity (p,x) ) & support it2 = Roots p & ( for x being Element of L holds it2 . x = multiplicity (p,x) ) implies it1 = it2 ) assume 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) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_ it1_._x_=_it2_._x let x be set ; ::_thesis: ( x in the carrier of L implies it1 . x = it2 . x ) assume x in the carrier of L ; ::_thesis: it1 . x = it2 . x then reconsider xx = x as Element of L ; thus it1 . x = multiplicity (p,xx) by A7 .= it2 . x by A8 ; ::_thesis: verum end; hence it1 = it2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def9 defines BRoots UPROOTS:def_9_:_ for L being domRing for p being non-zero Polynomial of L for b3 being bag of the carrier of L holds ( b3 = BRoots p iff ( support b3 = Roots p & ( for x being Element of L holds b3 . x = multiplicity (p,x) ) ) ); theorem Th54: :: UPROOTS:54 for L being domRing for x being Element of L holds BRoots <%(- x),(1. L)%> = ({x},1) -bag proof let L be domRing; ::_thesis: for x being Element of L holds BRoots <%(- x),(1. L)%> = ({x},1) -bag let x be Element of L; ::_thesis: BRoots <%(- x),(1. L)%> = ({x},1) -bag set r = <%(- x),(1. L)%>; Roots <%(- x),(1. L)%> = {x} by Th48; then A1: support (BRoots <%(- x),(1. L)%>) = {x} by Def9; A2: x in {x} by TARSKI:def_1; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_L_holds_ (BRoots_<%(-_x),(1._L)%>)_._i_=_(({x},1)_-bag)_._i let i be set ; ::_thesis: ( i in the carrier of L implies (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1 ) assume i in the carrier of L ; ::_thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1 then reconsider i1 = i as Element of L ; percases ( i = x or i <> x ) ; supposeA3: i = x ; ::_thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1 thus (BRoots <%(- x),(1. L)%>) . i = multiplicity (<%(- x),(1. L)%>,i1) by Def9 .= 1 by A3, Th53 .= (({x},1) -bag) . i by A2, A3, Th7 ; ::_thesis: verum end; suppose i <> x ; ::_thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1 then A4: not i in {x} by TARSKI:def_1; hence (BRoots <%(- x),(1. L)%>) . i = 0 by A1, PRE_POLY:def_7 .= (({x},1) -bag) . i by A4, Th6 ; ::_thesis: verum end; end; end; hence BRoots <%(- x),(1. L)%> = ({x},1) -bag by PBOOLE:3; ::_thesis: verum end; theorem Th55: :: UPROOTS:55 for L being domRing for x being Element of L for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x)) proof let L be domRing; ::_thesis: for x being Element of L for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x)) let x be Element of L; ::_thesis: for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x)) let p, q be non-zero Polynomial of L; ::_thesis: multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x)) set r = <%(- x),(1. L)%>; consider F being non empty finite Subset of NAT such that A1: F = { k where k is Element of NAT : ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq } and A2: multiplicity ((p *' q),x) = max F by Def8; consider f being non empty finite Subset of NAT such that A3: f = { k where k is Element of NAT : ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ 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 = (<%(- x),(1. L)%> `^ i) *' pq by A3; consider pq being Polynomial of L such that A7: p = (<%(- x),(1. L)%> `^ i) *' pq by A6; consider g being non empty finite Subset of NAT such that A8: g = { k where k is Element of NAT : ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ 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 = (<%(- x),(1. L)%> `^ k) *' pqq by A1; consider pqq being Polynomial of L such that A12: p *' q = (<%(- x),(1. L)%> `^ 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 = (<%(- x),(1. L)%> `^ j) *' qq by A8; consider qq being Polynomial of L such that A15: q = (<%(- x),(1. L)%> `^ j) *' qq by A14; A16: p *' q = (((<%(- x),(1. L)%> `^ i) *' pq) *' (<%(- x),(1. L)%> `^ j)) *' qq by A7, A15, POLYNOM3:33 .= (((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ j)) *' pq) *' qq by POLYNOM3:33 .= ((<%(- x),(1. L)%> `^ (i + j)) *' pq) *' qq by Th30 .= (<%(- x),(1. L)%> `^ (i + j)) *' (pq *' qq) by POLYNOM3:33 ; A17: now__::_thesis:_not_i_+_j_<_k assume i + j < k ; ::_thesis: contradiction then 0 + (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 = kk as Element of NAT by ORDINAL1:def_12; <%(- x),(1. L)%> `^ kij = (<%(- x),(1. L)%> `^ 1) *' (<%(- x),(1. L)%> `^ kk) by A19, Th30 .= <%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ kk) by POLYNOM5:16 ; then A20: (<%(- x),(1. L)%> `^ kij) *' pqq = <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ kk) *' pqq) by POLYNOM3:33; ( (0_. L) . 1 = 0. L & <%(- x),(1. L)%> . 1 = 1. L ) by FUNCOP_1:7, POLYNOM5:38; then A21: <%(- x),(1. L)%> `^ (i + j) <> 0_. L by Th29; k = kij + (i + j) ; then p *' q = ((<%(- x),(1. L)%> `^ (i + j)) *' (<%(- x),(1. L)%> `^ kij)) *' pqq by A12, Th30 .= (<%(- x),(1. L)%> `^ (i + j)) *' ((<%(- x),(1. L)%> `^ 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; percases ( x in Roots pq or x in Roots qq ) by A22, XBOOLE_0:def_3; suppose x in Roots pq ; ::_thesis: contradiction then x is_a_root_of pq by POLYNOM5:def_9; then pq = <%(- x),(1. L)%> *' (poly_quotient (pq,x)) by Th50; then p = ((<%(- x),(1. L)%> `^ i) *' <%(- x),(1. L)%>) *' (poly_quotient (pq,x)) by A7, POLYNOM3:33 .= ((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (pq,x)) by POLYNOM5:16 .= (<%(- x),(1. L)%> `^ (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; ::_thesis: verum end; suppose x in Roots qq ; ::_thesis: contradiction then x is_a_root_of qq by POLYNOM5:def_9; then qq = <%(- x),(1. L)%> *' (poly_quotient (qq,x)) by Th50; then q = ((<%(- x),(1. L)%> `^ j) *' <%(- x),(1. L)%>) *' (poly_quotient (qq,x)) by A15, POLYNOM3:33 .= ((<%(- x),(1. L)%> `^ j) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (qq,x)) by POLYNOM5:16 .= (<%(- x),(1. L)%> `^ (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; ::_thesis: verum end; end; end; i + j in F by A1, A16; then i + j <= k by A10, XXREAL_2:def_8; hence multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x)) by A2, A4, A9, A10, A5, A13, A17, XXREAL_0:1; ::_thesis: verum end; theorem Th56: :: UPROOTS:56 for L being domRing for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q) proof let L be domRing; ::_thesis: for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q) let p, q be non-zero Polynomial of L; ::_thesis: BRoots (p *' q) = (BRoots p) + (BRoots q) now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_L_holds_ (BRoots_(p_*'_q))_._i_=_((BRoots_p)_+_(BRoots_q))_._i let i be set ; ::_thesis: ( i in the carrier of L implies (BRoots (p *' q)) . i = ((BRoots p) + (BRoots q)) . i ) assume i in the carrier of L ; ::_thesis: (BRoots (p *' q)) . i = ((BRoots p) + (BRoots q)) . i 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 ; ::_thesis: verum end; hence BRoots (p *' q) = (BRoots p) + (BRoots q) by PBOOLE:3; ::_thesis: verum end; Lm2: now__::_thesis:_for_L_being_domRing for_p,_q_being_non-zero_Polynomial_of_L_holds_degree_(BRoots_(p_*'_q))_=_(degree_(BRoots_p))_+_(degree_(BRoots_q)) let L be domRing; ::_thesis: for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) let p, q be non-zero Polynomial of L; ::_thesis: degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) BRoots (p *' q) = (BRoots p) + (BRoots q) by Th56; hence degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) by Th15; ::_thesis: verum end; theorem Th57: :: UPROOTS:57 for L being domRing for p being non-zero Polynomial of L st len p = 1 holds degree (BRoots p) = 0 proof let L be domRing; ::_thesis: for p being non-zero Polynomial of L st len p = 1 holds degree (BRoots p) = 0 let p be non-zero Polynomial of L; ::_thesis: ( len p = 1 implies degree (BRoots p) = 0 ) assume len p = 1 ; ::_thesis: degree (BRoots p) = 0 then Roots p = {} by Th46; then support (BRoots p) = {} by Def9; then BRoots p = EmptyBag the carrier of L by BAGORDER:19; hence degree (BRoots p) = 0 by Th11; ::_thesis: verum end; theorem Th58: :: UPROOTS:58 for L being domRing for x being Element of L for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n proof let L be domRing; ::_thesis: for x being Element of L for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n let x be Element of L; ::_thesis: for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n set r = <%(- x),(1. L)%>; defpred S1[ Element of NAT ] means degree (BRoots (<%(- x),(1. L)%> `^ $1)) = $1; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] <%(- x),(1. L)%> `^ (n + 1) = (<%(- x),(1. L)%> `^ n) *' <%(- x),(1. L)%> by POLYNOM5:19; then A3: degree (BRoots (<%(- x),(1. L)%> `^ (n + 1))) = (degree (BRoots (<%(- x),(1. L)%> `^ n))) + (degree (BRoots <%(- x),(1. L)%>)) by Lm2 .= n + (degree (({x},1) -bag)) by A2, Th54 ; card {x} = 1 by CARD_1:30; hence S1[n + 1] by A3, Th13; ::_thesis: verum end; ( len (1_. L) = 1 & <%(- x),(1. L)%> `^ 0 = 1_. L ) by POLYNOM4:4, POLYNOM5:15; then A4: S1[ 0 ] by Th57; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); ::_thesis: verum end; theorem :: UPROOTS:59 for L being algebraic-closed domRing for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1 proof let L be algebraic-closed domRing; ::_thesis: for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1 let p be non-zero Polynomial of L; ::_thesis: degree (BRoots p) = (len p) -' 1 defpred S1[ 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 S1[n] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds S1[n] ) implies S1[k] ) assume A2: for n being Nat st n < k holds S1[n] ; ::_thesis: S1[k] let p be non-zero Polynomial of L; ::_thesis: ( len p = k & k > 0 implies degree (BRoots p) = (len p) -' 1 ) assume that A3: len p = k and A4: k > 0 ; ::_thesis: degree (BRoots p) = (len p) -' 1 A5: k >= 0 + 1 by A4, NAT_1:13; thus degree (BRoots p) = (len p) -' 1 ::_thesis: verum proof percases ( k = 1 or k > 1 ) by A5, XXREAL_0:1; supposeA6: k = 1 ; ::_thesis: degree (BRoots p) = (len p) -' 1 hence degree (BRoots p) = 1 - 1 by A3, Th57 .= (len p) -' 1 by A3, A6, XREAL_1:233 ; ::_thesis: verum end; supposeA7: k > 1 ; ::_thesis: degree (BRoots p) = (len p) -' 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 non empty finite 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 = q as non-zero Polynomial of L by A14, Th34; len q > 0 by Th17; then A15: len q >= 0 + 1 by NAT_1:13; thus degree (BRoots p) = (len p) -' 1 ::_thesis: verum proof len q > 0 by Th17; then A16: q . ((len q) -' 1) <> 0. L by Th18; len (<%(- x),(1. L)%> `^ l) > 0 by Th17; then (<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1) <> 0. L by Th18; then A17: ((<%(- x),(1. L)%> `^ l) . ((len (<%(- x),(1. L)%> `^ l)) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A16, VECTSP_2:def_1; A18: ((l * 2) - l) + 1 = l + 1 ; A19: len <%(- x),(1. L)%> = 2 by POLYNOM5:40; then A20: len (<%(- x),(1. L)%> `^ l) = ((l * 2) - l) + 1 by POLYNOM5:23; then A21: len (<%(- x),(1. L)%> `^ l) > 1 by A9, A11, A12, NAT_1:13; percases ( len q = 1 or len q > 1 ) by A15, XXREAL_0:1; supposeA22: len q = 1 ; ::_thesis: degree (BRoots p) = (len p) -' 1 A23: len p = ((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1 by A14, A17, POLYNOM4:10 .= len (<%(- x),(1. L)%> `^ l) by A22 ; thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2 .= (degree (BRoots (<%(- x),(1. L)%> `^ l))) + 0 by A22, Th57 .= (((2 * l) - l) + 1) - 1 by Th58 .= (len p) -' 1 by A3, A5, A20, A23, XREAL_1:233 ; ::_thesis: verum end; supposeA24: len q > 1 ; ::_thesis: degree (BRoots p) = (len p) -' 1 then A25: ( degree (BRoots (<%(- x),(1. L)%> `^ l)) = (l + 1) -' 1 & degree (BRoots q) = (len q) -' 1 ) by A2, A3, A14, A20, A21, Th36; thus degree (BRoots p) = (degree (BRoots (<%(- x),(1. L)%> `^ l))) + (degree (BRoots q)) by A14, Lm2 .= ((len (<%(- x),(1. L)%> `^ l)) -' 1) + ((len q) -' 1) by A19, A18, A25, POLYNOM5:23 .= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) -' 1) by A21, XREAL_1:233 .= ((len (<%(- x),(1. L)%> `^ l)) - 1) + ((len q) - 1) by A24, XREAL_1:233 .= (((len (<%(- x),(1. L)%> `^ l)) + (len q)) - 1) - 1 .= (len p) - 1 by A14, A17, POLYNOM4:10 .= (len p) -' 1 by A3, A7, XREAL_1:233 ; ::_thesis: verum end; end; end; end; end; end; end; A26: for n being Nat holds S1[n] from NAT_1:sch_4(A1); len p > 0 by Th17; hence degree (BRoots p) = (len p) -' 1 by A26; ::_thesis: verum end; definition let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; let c be Element of L; let n be Element of NAT ; func fpoly_mult_root (c,n) -> FinSequence of (Polynom-Ring L) means :Def10: :: UPROOTS:def 10 ( len it = n & ( for i being Element of NAT st i in dom it holds it . i = <%(- c),(1. L)%> ) ); existence ex b1 being FinSequence of (Polynom-Ring L) st ( len b1 = n & ( for i being Element of NAT st i in dom b1 holds b1 . i = <%(- c),(1. L)%> ) ) 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 ; ::_thesis: ( len f = n & ( for i being Element of NAT st i in dom f holds f . i = <%(- c),(1. L)%> ) ) thus A1: len f = n by CARD_1:def_7; ::_thesis: for i being Element of NAT st i in dom f holds f . i = <%(- c),(1. L)%> let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i = <%(- c),(1. L)%> ) assume i in dom f ; ::_thesis: f . i = <%(- c),(1. L)%> then i in Seg n by A1, FINSEQ_1:def_3; hence f . i = <%(- c),(1. L)%> by FUNCOP_1:7; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of (Polynom-Ring L) st len b1 = n & ( for i being Element of NAT st i in dom b1 holds b1 . i = <%(- c),(1. L)%> ) & len b2 = n & ( for i being Element of NAT st i in dom b2 holds b2 . i = <%(- c),(1. L)%> ) holds b1 = b2 proof let it1, it2 be FinSequence of (Polynom-Ring L); ::_thesis: ( len it1 = n & ( for i being Element of NAT st i in dom it1 holds it1 . i = <%(- c),(1. L)%> ) & len it2 = n & ( for i being Element of NAT st i in dom it2 holds it2 . i = <%(- c),(1. L)%> ) implies it1 = it2 ) assume 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)%> ; ::_thesis: it1 = it2 A6: dom it1 = dom it2 by A2, A4, FINSEQ_3:29; now__::_thesis:_for_x_being_Nat_st_x_in_dom_it1_holds_ it1_._x_=_it2_._x let x be Nat; ::_thesis: ( x in dom it1 implies it1 . x = it2 . x ) assume A7: x in dom it1 ; ::_thesis: it1 . x = it2 . x hence it1 . x = <%(- c),(1. L)%> by A3 .= it2 . x by A5, A6, A7 ; ::_thesis: verum end; hence it1 = it2 by A6, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def10 defines fpoly_mult_root UPROOTS:def_10_:_ for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for c being Element of L for n being Element of NAT for b4 being FinSequence of (Polynom-Ring L) holds ( b4 = fpoly_mult_root (c,n) iff ( len b4 = n & ( for i being Element of NAT st i in dom b4 holds b4 . i = <%(- c),(1. L)%> ) ) ); definition let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; let b be bag of the carrier of L; func poly_with_roots b -> Polynomial of L means :Def11: :: UPROOTS:def 11 ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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 ex b1 being Polynomial of L ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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))) ) & b1 = Product (FlattenSeq f) ) 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 H1( set ) -> FinSequence of (Polynom-Ring L) = 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 = H1(k) from FINSEQ_1:sch_2(); rng f c= the carrier of (Polynom-Ring L) * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in the carrier of (Polynom-Ring L) * ) assume x in rng f ; ::_thesis: x in the carrier of (Polynom-Ring L) * then consider i being Nat such that A3: ( i in dom f & f . i = x ) by FINSEQ_2:10; x = H1(i) by A2, A3; hence x in the carrier of (Polynom-Ring L) * by FINSEQ_1:def_11; ::_thesis: verum end; then reconsider f = 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 ; ::_thesis: ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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))) ) & it1 = Product (FlattenSeq f) ) take f ; ::_thesis: ex 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))) ) & it1 = Product (FlattenSeq f) ) take s ; ::_thesis: ( 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))) ) & it1 = Product (FlattenSeq f) ) thus len f = card (support b) by A1; ::_thesis: ( 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))) ) & it1 = Product (FlattenSeq f) ) thus s = canFS (support b) ; ::_thesis: ( ( for i being Element of NAT st i in dom f holds f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product (FlattenSeq f) ) thus for i being Element of NAT st i in dom f holds f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A2; ::_thesis: it1 = Product (FlattenSeq f) thus it1 = Product (FlattenSeq f) ; ::_thesis: verum end; uniqueness for b1, b2 being Polynomial of L st ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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))) ) & b1 = Product (FlattenSeq f) ) & ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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))) ) & b2 = Product (FlattenSeq f) ) holds b1 = b2 proof let it1, it2 be Polynomial of L; ::_thesis: ( ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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))) ) & it1 = Product (FlattenSeq f) ) & ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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))) ) & it2 = Product (FlattenSeq f) ) implies it1 = it2 ) 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) ; ::_thesis: ( for f being FinSequence of the carrier of (Polynom-Ring L) * for s being FinSequence of L holds ( not len f = card (support b) or not s = canFS (support b) or ex i being Element of NAT st ( i in dom f & not f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) or not it2 = Product (FlattenSeq f) ) or it1 = it2 ) 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) ; ::_thesis: it1 = it2 A11: dom f1 = dom f2 by A4, A8, FINSEQ_3:29; now__::_thesis:_for_i_being_Nat_st_i_in_dom_f1_holds_ f1_._i_=_f2_._i let i be Nat; ::_thesis: ( i in dom f1 implies f1 . i = f2 . i ) assume A12: i in dom f1 ; ::_thesis: f1 . i = f2 . i hence f1 . i = fpoly_mult_root ((s1 /. i),(b . (s1 /. i))) by A6 .= f2 . i by A5, A9, A11, A12 ; ::_thesis: verum end; hence it1 = it2 by A4, A7, A8, A10, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def11 defines poly_with_roots UPROOTS:def_11_:_ for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for b being bag of the carrier of L for b3 being Polynomial of L holds ( b3 = poly_with_roots b iff ex f being FinSequence of the carrier of (Polynom-Ring L) * ex 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))) ) & b3 = Product (FlattenSeq f) ) ); theorem Th60: :: UPROOTS:60 for L being non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%> proof let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%> 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 (EmptyBag the carrier of L)) and s = canFS (support (EmptyBag the carrier of L)) and for i being Element of NAT st i in dom f holds f . i = fpoly_mult_root ((s /. i),((EmptyBag the carrier of L) . (s /. i))) and A2: poly_with_roots (EmptyBag the carrier of L) = 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 poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%> by A2, Th31; ::_thesis: verum end; theorem Th61: :: UPROOTS:61 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%> proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%> let c be Element of L; ::_thesis: poly_with_roots (({c},1) -bag) = <%(- c),(1. 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 (({c},1) -bag)) and A2: s = canFS (support (({c},1) -bag)) and A3: for i being Element of NAT st i in dom f holds f . i = fpoly_mult_root ((s /. i),((({c},1) -bag) . (s /. i))) and A4: poly_with_roots (({c},1) -bag) = Product (FlattenSeq f) by Def11; A5: support (({c},1) -bag) = {c} by Th8; then A6: s = <*c*> by A2, Th4; A7: card (support (({c},1) -bag)) = 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),((({c},1) -bag) . (s /. 1))); c in {c} by TARSKI:def_1; then (({c},1) -bag) . (s /. 1) = 1 by A10, Th7; then A11: len (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) = 1 by Def10; then A12: 1 in dom (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) 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),((({c},1) -bag) . (s /. 1))) by A3, A8; fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1))) = <*((fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) /. 1)*> by A11, FINSEQ_5:14; hence poly_with_roots (({c},1) -bag) = (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) /. 1 by A4, A13, A14, FINSOP_1:11 .= (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) . 1 by A12, PARTFUN1:def_6 .= <%(- c),(1. L)%> by A10, A12, Def10 ; ::_thesis: verum end; theorem Th62: :: UPROOTS:62 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for b being bag of the carrier of L for f being FinSequence of the carrier of (Polynom-Ring L) * for 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 non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for b being bag of the carrier of L for f being FinSequence of the carrier of (Polynom-Ring L) * for 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 let b be bag of the carrier of L; ::_thesis: for f being FinSequence of the carrier of (Polynom-Ring L) * for 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 let f be FinSequence of the carrier of (Polynom-Ring L) * ; ::_thesis: for 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 let s be FinSequence of L; ::_thesis: ( 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))) ) implies len (FlattenSeq f) = degree b ) assume 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))) ; ::_thesis: len (FlattenSeq f) = degree b 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__::_thesis:_(_dom_(Card_f)_=_dom_g_&_(_for_i_being_Nat_st_i_in_dom_(Card_f)_holds_ Cf_._i_=_g_._i_)_) A8: rng s c= dom b proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s or x in dom b ) assume x in rng s ; ::_thesis: x in dom b then A9: x in support b by A2, FUNCT_2:def_3; support b c= dom b by PRE_POLY:37; hence x in dom b by A9; ::_thesis: verum end; thus dom (Card f) = dom f by CARD_3:def_2 .= dom g by A2, A6, A5, A8, RELAT_1:27 ; ::_thesis: for i being Nat st i in dom (Card f) holds Cf . i = g . i let i be Nat; ::_thesis: ( i in dom (Card f) implies Cf . i = g . i ) assume i in dom (Card f) ; ::_thesis: Cf . i = g . i 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 ; ::_thesis: verum end; len (FlattenSeq f) = Sum Cf by PRE_POLY:27; hence len (FlattenSeq f) = degree b by A4, A7, FINSEQ_1:13; ::_thesis: verum end; theorem Th63: :: UPROOTS:63 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for b being bag of the carrier of L for f being FinSequence of the carrier of (Polynom-Ring L) * for s being FinSequence of L for 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 non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for b being bag of the carrier of L for f being FinSequence of the carrier of (Polynom-Ring L) * for s being FinSequence of L for 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 ) ) let b be bag of the carrier of L; ::_thesis: for f being FinSequence of the carrier of (Polynom-Ring L) * for s being FinSequence of L for 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 ) ) let f be FinSequence of the carrier of (Polynom-Ring L) * ; ::_thesis: for s being FinSequence of L for 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 ) ) let s be FinSequence of L; ::_thesis: for 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 ) ) let c be Element of L; ::_thesis: ( 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))) ) implies ( ( 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 ) ) ) assume 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))) ; ::_thesis: ( ( 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 ) ) len f = len s by A1, A2, Th3; then A4: dom f = dom s by FINSEQ_3:29; hereby ::_thesis: ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) set X = { k where k is Element of NAT : k < b . c } ; set ff = FlattenSeq f; set Y = (FlattenSeq f) " {<%(- c),(1. L)%>}; assume c in support b ; ::_thesis: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c 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 S1[ 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 { k where k is Element of NAT : k < b . c } holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in { k where k is Element of NAT : k < b . c } implies ex y being set st S1[x,y] ) assume x in { k where k is Element of NAT : k < b . c } ; ::_thesis: ex y being set st S1[x,y] then consider k being Element of NAT such that A8: x = k and k < b . c ; take (Sum (Card (f | (i -' 1)))) + (1 + k) ; ::_thesis: S1[x,(Sum (Card (f | (i -' 1)))) + (1 + k)] thus S1[x,(Sum (Card (f | (i -' 1)))) + (1 + k)] by A8; ::_thesis: verum end; consider g being Function such that A9: dom g = { k where k is Element of NAT : k < b . c } and A10: for x being set st x in { k where k is Element of NAT : k < b . c } holds S1[x,g . x] from CLASSES1:sch_1(A7); A11: s /. i = c by A5, A6, PARTFUN1:def_6; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_g_implies_y_in_(FlattenSeq_f)_"_{<%(-_c),(1._L)%>}_)_&_(_y_in_(FlattenSeq_f)_"_{<%(-_c),(1._L)%>}_implies_y_in_rng_g_)_) let y be set ; ::_thesis: ( ( y in rng g implies y in (FlattenSeq f) " {<%(- c),(1. L)%>} ) & ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g ) ) A12: <%(- c),(1. L)%> . 0 = - c by POLYNOM5:38; hereby ::_thesis: ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g ) assume y in rng g ; ::_thesis: y in (FlattenSeq f) " {<%(- c),(1. L)%>} 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, NAT_1: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 (FlattenSeq f) & (f . i) . (1 + n) = (FlattenSeq f) . ((Sum (Card (f | (i -' 1)))) + (1 + n)) ) by A4, A5, A19, PRE_POLY:30; hence y in (FlattenSeq f) " {<%(- c),(1. L)%>} by A14, A16, A20, FUNCT_1:def_7; ::_thesis: verum end; assume A21: y in (FlattenSeq f) " {<%(- c),(1. L)%>} ; ::_thesis: y in rng g then reconsider yn = y as Element of NAT ; A22: (FlattenSeq f) . y in {<%(- c),(1. L)%>} by A21, FUNCT_1:def_7; y in dom (FlattenSeq f) 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 = (FlattenSeq f) . 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 = 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 { k where k is Element of NAT : k < b . c } ; 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; ::_thesis: verum end; then A32: rng g = (FlattenSeq f) " {<%(- c),(1. L)%>} by TARSKI:1; g is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 g or not x2 in proj1 g or not g . x1 = g . x2 or x1 = x2 ) assume that A33: ( x1 in dom g & x2 in dom g ) and A34: g . x1 = g . x2 ; ::_thesis: x1 = 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 x1 = x2 by A34; ::_thesis: verum end; then ( b . c = { k where k is Element of NAT : k < b . c } & { k where k is Element of NAT : k < b . c } ,(FlattenSeq f) " {<%(- c),(1. L)%>} are_equipotent ) by A9, A32, AXIOMS:4, WELLORD2:def_4; hence card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c by CARD_1:def_2; ::_thesis: verum end; assume that A35: not c in support b and A36: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) <> 0 ; ::_thesis: contradiction 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 = 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; ::_thesis: verum end; theorem Th64: :: UPROOTS:64 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; ::_thesis: for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2) let b1, b2 be bag of the carrier of L; ::_thesis: poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2) set b = b1 + b2; A1: support (b1 + b2) = (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 (b1 + b2)) and A11: s = canFS (support (b1 + b2)) and A12: for i being Element of NAT st i in dom f holds f . i = fpoly_mult_root ((s /. i),((b1 + b2) . (s /. i))) and A13: poly_with_roots (b1 + b2) = Product (FlattenSeq f) by Def11; set ff = FlattenSeq f; set ff1 = FlattenSeq f1; set ff2 = FlattenSeq f2; A14: len (FlattenSeq f) = degree (b1 + b2) by A10, A11, A12, Th62; A15: len (FlattenSeq f2) = degree b2 by A2, A3, A4, Th62; set g = (FlattenSeq f1) ^ (FlattenSeq f2); len ((FlattenSeq f1) ^ (FlattenSeq f2)) = (len (FlattenSeq f1)) + (len (FlattenSeq f2)) by FINSEQ_1:22 .= (degree b1) + (degree b2) by A6, A7, A8, A15, Th62 .= degree (b1 + b2) by Th15 ; then A16: dom (FlattenSeq f) = dom ((FlattenSeq f1) ^ (FlattenSeq f2)) by A14, FINSEQ_3:29; A17: len s = card (support (b1 + b2)) by A11, Th3; now__::_thesis:_for_x_being_set_holds_card_(Coim_((FlattenSeq_f),x))_=_card_(Coim_(((FlattenSeq_f1)_^_(FlattenSeq_f2)),x)) let x be set ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1)) percases ( x in rng (FlattenSeq f) or not x in rng (FlattenSeq f) ) ; suppose x in rng (FlattenSeq f) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1)) then consider k being Nat such that A18: k in dom (FlattenSeq f) and A19: (FlattenSeq f) . 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 = (FlattenSeq f) . k by A18, PRE_POLY:29; f . i = fpoly_mult_root ((s /. i),((b1 + b2) . (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 (b1 + b2) by A11, FUNCT_2:def_3; A25: card (((FlattenSeq f1) ^ (FlattenSeq f2)) " {x}) = (card ((FlattenSeq f1) " {x})) + (card ((FlattenSeq f2) " {x})) by FINSEQ_3:57; percases ( ( s /. i in support b1 & not s /. i in support b2 ) or ( not s /. i in support b1 & s /. i in support b2 ) or ( s /. i in support b1 & s /. i in support b2 ) ) by A1, A24, XBOOLE_0:def_3; supposeA26: ( s /. i in support b1 & not s /. i in support b2 ) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1)) then A27: card ((FlattenSeq f2) " {x}) = 0 by A2, A3, A4, A19, A22, A23, Th63; thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (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 by A26, PRE_POLY:def_7 .= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A26, A27, Th63 ; ::_thesis: verum end; supposeA28: ( not s /. i in support b1 & s /. i in support b2 ) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1)) then A29: card ((FlattenSeq f2) " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th63; thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th63 .= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def_5 .= 0 + (b2 . (s /. i)) by A28, PRE_POLY:def_7 .= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A28, A29, Th63 ; ::_thesis: verum end; supposeA30: ( s /. i in support b1 & s /. i in support b2 ) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1)) then A31: card ((FlattenSeq f2) " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th63; thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th63 .= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def_5 .= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A30, A31, Th63 ; ::_thesis: verum end; end; end; supposeA32: not x in rng (FlattenSeq f) ; ::_thesis: card (Coim ((FlattenSeq f),b1)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b1)) now__::_thesis:_not_x_in_rng_((FlattenSeq_f1)_^_(FlattenSeq_f2)) assume x in rng ((FlattenSeq f1) ^ (FlattenSeq f2)) ; ::_thesis: contradiction then A33: x in (rng (FlattenSeq f1)) \/ (rng (FlattenSeq f2)) by FINSEQ_1:31; percases ( x in rng (FlattenSeq f1) or x in rng (FlattenSeq f2) ) by A33, XBOOLE_0:def_3; suppose x in rng (FlattenSeq f1) ; ::_thesis: contradiction then consider k being Nat such that A34: k in dom (FlattenSeq f1) and A35: (FlattenSeq f1) . 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 = (FlattenSeq f1) . 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 (b1 + b2) by A1, XBOOLE_0:def_3; then (b1 + b2) . (s1 /. i) <> 0 by PRE_POLY:def_7; then A41: 0 + 1 <= (b1 + b2) . (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),((b1 + b2) . (s /. l))) by A12; then len (f . l) = (b1 + b2) . (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 (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A45, PRE_POLY:30; then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:3; hence contradiction by A32, A35, A38, A39, A43, A46, A44, A47, Def10; ::_thesis: verum end; suppose x in rng (FlattenSeq f2) ; ::_thesis: contradiction then consider k being Nat such that A48: k in dom (FlattenSeq f2) and A49: (FlattenSeq f2) . 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 = (FlattenSeq f2) . 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 (b1 + b2) by A1, XBOOLE_0:def_3; then (b1 + b2) . (s2 /. i) <> 0 by PRE_POLY:def_7; then A55: 0 + 1 <= (b1 + b2) . (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),((b1 + b2) . (s /. l))) by A12; then len (f . l) = (b1 + b2) . (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 (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A59, PRE_POLY:30; then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:3; hence contradiction by A32, A49, A52, A53, A57, A60, A58, A61, Def10; ::_thesis: verum end; end; end; then ((FlattenSeq f1) ^ (FlattenSeq f2)) " {x} = {} by FUNCT_1:72; hence card (Coim ((FlattenSeq f),x)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A32, FUNCT_1:72; ::_thesis: verum end; end; end; then FlattenSeq f,(FlattenSeq f1) ^ (FlattenSeq f2) 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 ; ::_thesis: verum end; theorem :: UPROOTS:65 for L being algebraic-closed domRing for 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; ::_thesis: for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds p = poly_with_roots (BRoots p) let p be non-zero Polynomial of L; ::_thesis: ( p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) ) assume A1: p . ((len p) -' 1) = 1. L ; ::_thesis: p = poly_with_roots (BRoots p) defpred S1[ 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 + 1 by NAT_1:13; A3: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that A4: n >= 1 and A5: S1[n] ; ::_thesis: S1[n + 1] let p be non-zero Polynomial of L; ::_thesis: ( len p = n + 1 & n + 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) ) assume that A6: len p = n + 1 and n + 1 >= 1 and A7: p . ((len p) -' 1) = 1. L ; ::_thesis: p = poly_with_roots (BRoots p) 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 = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A8, Th50; then reconsider q = poly_quotient (p,x) as non-zero Polynomial of L by Th34; A10: len <%(- x),(1. L)%> = 2 by POLYNOM5:40; then A11: <%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 1) <> 0. L by Th18; len q > 0 by Th17; then q . ((len q) -' 1) <> 0. L by Th18; then (<%(- x),(1. L)%> . ((len <%(- x),(1. L)%>) -' 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 <%(- x),(1. L)%> = ({x},1) -bag by Th54; then BRoots p = (({x},1) -bag) + (BRoots q) by A9, Th56; hence p = poly_with_roots (BRoots p) by A9, A13, A14, Th64; ::_thesis: verum end; A15: S1[1] proof let p be non-zero Polynomial of L; ::_thesis: ( len p = 1 & 1 >= 1 & p . ((len p) -' 1) = 1. L implies p = poly_with_roots (BRoots p) ) assume that A16: len p = 1 and 1 >= 1 and A17: p . ((len p) -' 1) = 1. L ; ::_thesis: p = poly_with_roots (BRoots p) 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 ; ::_thesis: verum end; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A15, A3); hence p = poly_with_roots (BRoots p) by A1, A2; ::_thesis: verum end; theorem :: UPROOTS:66 for L being comRing for s being non empty finite Subset of L for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT for 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; ::_thesis: for s being non empty finite Subset of L for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT for 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 set cL = the carrier of L; set cPRL = the carrier of (Polynom-Ring L); let s be non empty finite Subset of the carrier of L; ::_thesis: for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT for 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 let f be FinSequence of the carrier of (Polynom-Ring L); ::_thesis: ( len f = card s & ( for i being Element of NAT for c being Element of L st i in dom f & c = (canFS s) . i holds f . i = <%(- c),(1. L)%> ) implies poly_with_roots ((s,1) -bag) = Product f ) assume that A1: len f = card s and A2: for i being Element of NAT for c being Element of the carrier of L st i in dom f & c = (canFS s) . i holds f . i = <%(- c),(1. L)%> ; ::_thesis: poly_with_roots ((s,1) -bag) = Product f set cs = canFS s; A3: rng (canFS s) = s by FUNCT_2:def_3; defpred S1[ Element of NAT ] means ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st ( t = rng ((canFS s) | (Seg $1)) & g = f | (Seg $1) & poly_with_roots ((t,1) -bag) = Product g ); A4: len (canFS s) = card s by Th3; then A5: dom f = dom (canFS s) by A1, FINSEQ_3:29; A6: for j being Element of NAT st 1 <= j & j < len f & S1[j] holds S1[j + 1] proof let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] ) assume that A7: 1 <= j and A8: j < len f ; ::_thesis: ( not S1[j] or S1[j + 1] ) reconsider g1 = f | (Seg (j + 1)) as FinSequence of the carrier of (Polynom-Ring L) 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 (canFS s) by A1, A4, A9, FINSEQ_3:25; then (canFS s) . (j + 1) in s by FINSEQ_2:11; then reconsider csj1 = (canFS s) . (j + 1) as Element of the carrier of L ; A12: g1 . (j + 1) = f . (j + 1) by FINSEQ_1:4, FUNCT_1:49 .= <%(- csj1),(1. L)%> by A2, A5, A11 ; reconsider csja1 = (canFS s) | (Seg (j + 1)) as FinSequence of s by FINSEQ_1:18; reconsider csja = (canFS s) | (Seg j) as FinSequence of s by FINSEQ_1:18; given t being finite Subset of the carrier of L, g being FinSequence of the carrier of (Polynom-Ring L) such that A13: t = rng ((canFS s) | (Seg j)) and A14: g = f | (Seg j) and A15: poly_with_roots ((t,1) -bag) = Product g ; ::_thesis: S1[j + 1] 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 \/ ((canFS s) | {(j + 1)}) by RELAT_1:78; (canFS s) | {(j + 1)} = (j + 1) .--> csj1 by A11, FUNCT_7:6; then rng ((canFS s) | {(j + 1)}) = {csj1} by FUNCOP_1:8; then A18: rng csja1 = t \/ {csj1} by A13, A17, RELAT_1:12; reconsider epj1 = <%(- csj1),(1. L)%> as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def_10; reconsider pj1 = poly_with_roots (({csj1},1) -bag) as Polynomial of L ; A19: pj1 = epj1 by Th61; reconsider t1 = rng csja1 as finite Subset of the carrier of L by A18; take t1 ; ::_thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st ( t1 = rng ((canFS s) | (Seg (j + 1))) & g = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g ) take g1 ; ::_thesis: ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g1 ) thus ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) ) ; ::_thesis: poly_with_roots ((t1,1) -bag) = Product g1 t misses {csj1} proof assume not t misses {csj1} ; ::_thesis: contradiction 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 ((canFS s) | (Seg j)) and A23: x = ((canFS s) | (Seg j)) . i by A13, FUNCT_1:def_3; A24: i in Seg j by A22, RELAT_1:57; reconsider i = 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 = (canFS s) . i by A22, A23, FUNCT_1:47; hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7; ::_thesis: verum 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 ; ::_thesis: verum end; f | (Seg (len f)) is FinSequence by FINSEQ_1:18; then A27: ( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f ) by FINSEQ_1:18, FINSEQ_2:20; A28: 0 + 1 <= len f by A1, NAT_1:13; A29: S1[1] proof 1 in dom (canFS s) by A1, A4, A28, FINSEQ_3:25; then reconsider cs1 = (canFS s) . 1 as Element of s by FINSEQ_2:11; reconsider g = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring L) by FINSEQ_1:18; reconsider cs1a = (canFS s) | (Seg 1) as FinSequence of s by FINSEQ_1:18; A30: cs1 in the carrier of L ; A31: 1 in Seg 1 by FINSEQ_1:1; then A32: cs1a . 1 = cs1 by FUNCT_1:49; reconsider cs1 = (canFS s) . 1 as Element of the carrier of L by A30; reconsider t = {cs1} as finite Subset of the carrier of L ; take t ; ::_thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g ) take g ; ::_thesis: ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product 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 ((canFS s) | (Seg 1)) & g = f | (Seg 1) ) by A33, A32, FINSEQ_1:39; ::_thesis: poly_with_roots ((t,1) -bag) = Product g consider p1 being Element of the carrier of (Polynom-Ring L) 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 the carrier of (Polynom-Ring L) by FINSEQ_2:11; A37: g . 1 = f1 by A31, FUNCT_1:49; f1 = <%(- cs1),(1. L)%> by A2, A36; hence poly_with_roots ((t,1) -bag) = Product g by A37, A35, Th61; ::_thesis: verum end; for i being Element of NAT st 1 <= i & i <= len f holds S1[i] from INT_1:sch_7(A29, A6); then ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st ( t = rng ((canFS s) | (Seg (len f))) & g = f | (Seg (len f)) & poly_with_roots ((t,1) -bag) = Product g ) by A28; hence poly_with_roots ((s,1) -bag) = Product f by A1, A4, A27, A3, FINSEQ_2:20; ::_thesis: verum end; theorem :: UPROOTS:67 for L being non trivial comRing for s being non empty finite Subset of L for x being Element of L for f being FinSequence of L st len f = card s & ( for i being Element of NAT for 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; ::_thesis: for s being non empty finite Subset of L for x being Element of L for f being FinSequence of L st len f = card s & ( for i being Element of NAT for 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 set cL = the carrier of L; let s be non empty finite Subset of the carrier of L; ::_thesis: for x being Element of L for f being FinSequence of L st len f = card s & ( for i being Element of NAT for 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 let x be Element of the carrier of L; ::_thesis: for f being FinSequence of L st len f = card s & ( for i being Element of NAT for 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 let f be FinSequence of L; ::_thesis: ( len f = card s & ( for i being Element of NAT for c being Element of L st i in dom f & c = (canFS s) . i holds f . i = eval (<%(- c),(1. L)%>,x) ) implies eval ((poly_with_roots ((s,1) -bag)),x) = Product f ) assume that A1: len f = card s and A2: for i being Element of NAT for c being Element of the carrier of L st i in dom f & c = (canFS s) . i holds f . i = eval (<%(- c),(1. L)%>,x) ; ::_thesis: eval ((poly_with_roots ((s,1) -bag)),x) = Product f set cs = canFS s; A3: rng (canFS s) = s by FUNCT_2:def_3; defpred S1[ Element of NAT ] means ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of L st ( t = rng ((canFS s) | (Seg $1)) & g = f | (Seg $1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g ); A4: len (canFS s) = card s by Th3; then A5: dom f = dom (canFS s) by A1, FINSEQ_3:29; A6: for j being Element of NAT st 1 <= j & j < len f & S1[j] holds S1[j + 1] proof let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] ) assume that A7: 1 <= j and A8: j < len f ; ::_thesis: ( not S1[j] or S1[j + 1] ) reconsider g1 = f | (Seg (j + 1)) as FinSequence of the carrier of L 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 (canFS s) by A1, A4, A9, FINSEQ_3:25; then (canFS s) . (j + 1) in s by FINSEQ_2:11; then reconsider csj1 = (canFS s) . (j + 1) as Element of the carrier of L ; 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 = (canFS s) | (Seg (j + 1)) as FinSequence of s by FINSEQ_1:18; reconsider csja = (canFS s) | (Seg j) as FinSequence of s by FINSEQ_1:18; given t being finite Subset of the carrier of L, g being FinSequence of the carrier of L such that A13: t = rng ((canFS s) | (Seg j)) and A14: g = f | (Seg j) and A15: eval ((poly_with_roots ((t,1) -bag)),x) = Product g ; ::_thesis: S1[j + 1] 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 \/ ((canFS s) | {(j + 1)}) by RELAT_1:78; (canFS s) | {(j + 1)} = (j + 1) .--> csj1 by A11, FUNCT_7:6; then rng ((canFS s) | {(j + 1)}) = {csj1} by FUNCOP_1:8; then A18: rng csja1 = t \/ {csj1} by A13, A17, RELAT_1:12; then reconsider t1 = rng csja1 as finite Subset of the carrier of L ; take t1 ; ::_thesis: ex g being FinSequence of the carrier of L st ( t1 = rng ((canFS s) | (Seg (j + 1))) & g = f | (Seg (j + 1)) & eval ((poly_with_roots ((t1,1) -bag)),x) = Product g ) take g1 ; ::_thesis: ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & eval ((poly_with_roots ((t1,1) -bag)),x) = Product g1 ) thus ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) ) ; ::_thesis: eval ((poly_with_roots ((t1,1) -bag)),x) = Product g1 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 t misses {csj1} ; ::_thesis: contradiction 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 ((canFS s) | (Seg j)) and A23: x = ((canFS s) | (Seg j)) . i by A13, FUNCT_1:def_3; A24: i in Seg j by A22, RELAT_1:57; reconsider i = 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 = (canFS s) . i by A22, A23, FUNCT_1:47; hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7; ::_thesis: verum 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 ; ::_thesis: verum end; f | (Seg (len f)) is FinSequence by FINSEQ_1:18; then A27: ( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f ) by FINSEQ_1:18, FINSEQ_2:20; A28: 0 + 1 <= len f by A1, NAT_1:13; A29: S1[1] proof 1 in dom (canFS s) by A1, A4, A28, FINSEQ_3:25; then reconsider cs1 = (canFS s) . 1 as Element of s by FINSEQ_2:11; reconsider g = f | (Seg 1) as FinSequence of the carrier of L by FINSEQ_1:18; reconsider cs1a = (canFS s) | (Seg 1) as FinSequence of s by FINSEQ_1:18; A30: cs1 in the carrier of L ; A31: 1 in Seg 1 by FINSEQ_1:1; then A32: cs1a . 1 = cs1 by FUNCT_1:49; reconsider cs1 = (canFS s) . 1 as Element of the carrier of L by A30; reconsider t = {cs1} as finite Subset of the carrier of L ; take t ; ::_thesis: ex g being FinSequence of the carrier of L st ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g ) take g ; ::_thesis: ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product 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 ((canFS s) | (Seg 1)) & g = f | (Seg 1) ) by A33, A32, FINSEQ_1:39; ::_thesis: eval ((poly_with_roots ((t,1) -bag)),x) = Product g consider p1 being Element of the carrier of L 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 the carrier of L by FINSEQ_2:11; A37: g . 1 = f1 by A31, FUNCT_1:49; f1 = eval (<%(- cs1),(1. L)%>,x) by A2, A36; hence eval ((poly_with_roots ((t,1) -bag)),x) = Product g by A37, A35, Th61; ::_thesis: verum end; for i being Element of NAT st 1 <= i & i <= len f holds S1[i] from INT_1:sch_7(A29, A6); then ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of L st ( t = rng ((canFS s) | (Seg (len f))) & g = f | (Seg (len f)) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g ) by A28; hence eval ((poly_with_roots ((s,1) -bag)),x) = Product f by A1, A4, A27, A3, FINSEQ_2:20; ::_thesis: verum end;