:: POLYNOM1 semantic presentation begin registration cluster non empty degenerated right_complementable right-distributive right_unital add-associative right_zeroed -> non empty trivial right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ; coherence for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st b1 is degenerated holds b1 is trivial proof let L be non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is degenerated implies L is trivial ) assume A1: 0. L = 1. L ; :: according to STRUCT_0:def_8 ::_thesis: L is trivial let u be Element of L; :: according to STRUCT_0:def_18 ::_thesis: u = 0. L thus u = u * (1. L) by VECTSP_1:def_4 .= 0. L by A1, VECTSP_1:6 ; ::_thesis: verum end; end; registration cluster non empty non trivial right_complementable right-distributive right_unital add-associative right_zeroed -> non empty non degenerated right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ; coherence for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st not b1 is trivial holds not b1 is degenerated ; end; theorem Th1: :: POLYNOM1:1 for K being non empty addLoopStr for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds dom (p1 + p2) = dom p1 proof let K be non empty addLoopStr ; ::_thesis: for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds dom (p1 + p2) = dom p1 let p1, p2 be FinSequence of the carrier of K; ::_thesis: ( dom p1 = dom p2 implies dom (p1 + p2) = dom p1 ) assume A1: dom p1 = dom p2 ; ::_thesis: dom (p1 + p2) = dom p1 A2: ( rng <:p1,p2:> c= [:(rng p1),(rng p2):] & [:(rng p1),(rng p2):] c= [: the carrier of K, the carrier of K:] ) by FUNCT_3:51, ZFMISC_1:96; A3: [: the carrier of K, the carrier of K:] = dom the addF of K by FUNCT_2:def_1; thus dom (p1 + p2) = dom ( the addF of K .: (p1,p2)) by FVSUM_1:def_3 .= dom <:p1,p2:> by A2, A3, RELAT_1:27, XBOOLE_1:1 .= (dom p1) /\ (dom p2) by FUNCT_3:def_7 .= dom p1 by A1 ; ::_thesis: verum end; theorem Th2: :: POLYNOM1:2 for L being non empty addLoopStr for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F proof let L be non empty addLoopStr ; ::_thesis: for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F let F be FinSequence of the carrier of L * ; ::_thesis: dom (Sum F) = dom F len (Sum F) = len F by MATRLIN:def_6; hence dom (Sum F) = dom F by FINSEQ_3:29; ::_thesis: verum end; theorem Th3: :: POLYNOM1:3 for L being non empty addLoopStr for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L proof let L be non empty addLoopStr ; ::_thesis: for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L let F be FinSequence of the carrier of L * ; ::_thesis: Sum (<*> ( the carrier of L *)) = <*> the carrier of L dom (Sum (<*> ( the carrier of L *))) = dom (<*> ( the carrier of L *)) by Th2; hence Sum (<*> ( the carrier of L *)) = <*> the carrier of L ; ::_thesis: verum end; theorem Th4: :: POLYNOM1:4 for L being non empty addLoopStr for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*> proof let L be non empty addLoopStr ; ::_thesis: for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*> let p be Element of the carrier of L * ; ::_thesis: <*(Sum p)*> = Sum <*p*> A1: now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*p*>_holds_ <*(Sum_p)*>_/._i_=_Sum_(<*p*>_/._i) let i be Nat; ::_thesis: ( i in dom <*p*> implies <*(Sum p)*> /. i = Sum (<*p*> /. i) ) assume i in dom <*p*> ; ::_thesis: <*(Sum p)*> /. i = Sum (<*p*> /. i) then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then A2: i = 1 by TARSKI:def_1; hence <*(Sum p)*> /. i = Sum p by FINSEQ_4:16 .= Sum (<*p*> /. i) by A2, FINSEQ_4:16 ; ::_thesis: verum end; A3: dom <*(Sum p)*> = Seg 1 by FINSEQ_1:38 .= dom <*p*> by FINSEQ_1:38 ; then len <*(Sum p)*> = len <*p*> by FINSEQ_3:29; hence <*(Sum p)*> = Sum <*p*> by A3, A1, MATRLIN:def_6; ::_thesis: verum end; theorem Th5: :: POLYNOM1:5 for L being non empty addLoopStr for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G) proof let L be non empty addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G) let F, G be FinSequence of the carrier of L * ; ::_thesis: Sum (F ^ G) = (Sum F) ^ (Sum G) A1: dom (Sum F) = dom F by Th2; A2: dom (Sum G) = dom G by Th2; A3: len ((Sum F) ^ (Sum G)) = (len (Sum F)) + (len (Sum G)) by FINSEQ_1:22 .= (len F) + (len (Sum G)) by A1, FINSEQ_3:29 .= (len F) + (len G) by A2, FINSEQ_3:29 .= len (F ^ G) by FINSEQ_1:22 ; then A4: dom ((Sum F) ^ (Sum G)) = dom (F ^ G) by FINSEQ_3:29; A5: len (Sum F) = len F by A1, FINSEQ_3:29; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(F_^_G)_holds_ ((Sum_F)_^_(Sum_G))_/._i_=_Sum_((F_^_G)_/._i) let i be Nat; ::_thesis: ( i in dom (F ^ G) implies ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1) ) assume A6: i in dom (F ^ G) ; ::_thesis: ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1) percases ( i in dom F or ex n being Nat st ( n in dom G & i = (len F) + n ) ) by A6, FINSEQ_1:25; supposeA7: i in dom F ; ::_thesis: ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1) thus ((Sum F) ^ (Sum G)) /. i = ((Sum F) ^ (Sum G)) . i by A4, A6, PARTFUN1:def_6 .= (Sum F) . i by A1, A7, FINSEQ_1:def_7 .= (Sum F) /. i by A1, A7, PARTFUN1:def_6 .= Sum (F /. i) by A1, A7, MATRLIN:def_6 .= Sum ((F ^ G) /. i) by A7, FINSEQ_4:68 ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom G & i = (len F) + n ) ; ::_thesis: ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1) then consider n being Nat such that A8: n in dom G and A9: i = (len F) + n ; thus ((Sum F) ^ (Sum G)) /. i = ((Sum F) ^ (Sum G)) . i by A4, A6, PARTFUN1:def_6 .= (Sum G) . n by A2, A5, A8, A9, FINSEQ_1:def_7 .= (Sum G) /. n by A2, A8, PARTFUN1:def_6 .= Sum (G /. n) by A2, A8, MATRLIN:def_6 .= Sum ((F ^ G) /. i) by A8, A9, FINSEQ_4:69 ; ::_thesis: verum end; end; end; hence Sum (F ^ G) = (Sum F) ^ (Sum G) by A3, A4, MATRLIN:def_6; ::_thesis: verum end; definition let L be non empty multMagma ; let p be FinSequence of the carrier of L; let a be Element of L; redefine func a * p means :Def1: :: POLYNOM1:def 1 ( dom it = dom p & ( for i being set st i in dom p holds it /. i = a * (p /. i) ) ); compatibility for b1 being FinSequence of the carrier of L holds ( b1 = a * p iff ( dom b1 = dom p & ( for i being set st i in dom p holds b1 /. i = a * (p /. i) ) ) ) proof A1: now__::_thesis:_for_G_being_FinSequence_of_the_carrier_of_L_st_dom_G_=_dom_p_&_(_for_i_being_set_st_i_in_dom_p_holds_ G_/._i_=_a_*_(p_/._i)_)_holds_ G_=_a_*_p set R = (a multfield) * p; let G be FinSequence of the carrier of L; ::_thesis: ( dom G = dom p & ( for i being set st i in dom p holds G /. i = a * (p /. i) ) implies G = a * p ) assume that A2: dom G = dom p and A3: for i being set st i in dom p holds G /. i = a * (p /. i) ; ::_thesis: G = a * p A4: for k being set st k in dom G holds G . k = ((a multfield) * p) . k proof let k be set ; ::_thesis: ( k in dom G implies G . k = ((a multfield) * p) . k ) assume A5: k in dom G ; ::_thesis: G . k = ((a multfield) * p) . k then G . k = G /. k by PARTFUN1:def_6 .= a * (p /. k) by A2, A3, A5 .= (a multfield) . (p /. k) by FVSUM_1:49 .= (a multfield) . (p . k) by A2, A5, PARTFUN1:def_6 .= ((a multfield) * p) . k by A2, A5, FUNCT_1:13 ; hence G . k = ((a multfield) * p) . k ; ::_thesis: verum end; ( rng p c= the carrier of L & dom (a multfield) = the carrier of L ) by FUNCT_2:def_1; then dom G = dom ((a multfield) * p) by A2, RELAT_1:27; then G = (a multfield) * p by A4, FUNCT_1:2; hence G = a * p by FVSUM_1:def_6; ::_thesis: verum end; set F = a * p; A6: rng p c= dom (a multfield) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in dom (a multfield) ) dom (a multfield) = the carrier of L by FUNCT_2:def_1; hence ( not x in rng p or x in dom (a multfield) ) ; ::_thesis: verum end; A7: a * p = (a multfield) * p by FVSUM_1:def_6; then A8: dom (a * p) = dom p by A6, RELAT_1:27; for i being set st i in dom p holds (a * p) /. i = a * (p /. i) proof let i be set ; ::_thesis: ( i in dom p implies (a * p) /. i = a * (p /. i) ) assume A9: i in dom p ; ::_thesis: (a * p) /. i = a * (p /. i) (a * p) . i = ((a multfield) * p) . i by FVSUM_1:def_6 .= (a multfield) . (p . i) by A9, FUNCT_1:13 .= (a multfield) . (p /. i) by A9, PARTFUN1:def_6 .= a * (p /. i) by FVSUM_1:49 ; hence (a * p) /. i = a * (p /. i) by A8, A9, PARTFUN1:def_6; ::_thesis: verum end; hence for b1 being FinSequence of the carrier of L holds ( b1 = a * p iff ( dom b1 = dom p & ( for i being set st i in dom p holds b1 /. i = a * (p /. i) ) ) ) by A7, A6, A1, RELAT_1:27; ::_thesis: verum end; end; :: deftheorem Def1 defines * POLYNOM1:def_1_:_ for L being non empty multMagma for p being FinSequence of the carrier of L for a being Element of L for b4 being FinSequence of the carrier of L holds ( b4 = a * p iff ( dom b4 = dom p & ( for i being set st i in dom p holds b4 /. i = a * (p /. i) ) ) ); definition let L be non empty multMagma ; let p be FinSequence of the carrier of L; let a be Element of L; funcp * a -> FinSequence of the carrier of L means :Def2: :: POLYNOM1:def 2 ( dom it = dom p & ( for i being set st i in dom p holds it /. i = (p /. i) * a ) ); existence ex b1 being FinSequence of the carrier of L st ( dom b1 = dom p & ( for i being set st i in dom p holds b1 /. i = (p /. i) * a ) ) proof deffunc H1( set ) -> Element of the carrier of L = (p /. $1) * a; consider f being FinSequence of the carrier of L such that A1: len f = len p and A2: for j being Nat st j in dom f holds f /. j = H1(j) from FINSEQ_4:sch_2(); take f ; ::_thesis: ( dom f = dom p & ( for i being set st i in dom p holds f /. i = (p /. i) * a ) ) thus A3: dom f = dom p by A1, FINSEQ_3:29; ::_thesis: for i being set st i in dom p holds f /. i = (p /. i) * a let j be set ; ::_thesis: ( j in dom p implies f /. j = (p /. j) * a ) assume j in dom p ; ::_thesis: f /. j = (p /. j) * a hence f /. j = (p /. j) * a by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of the carrier of L st dom b1 = dom p & ( for i being set st i in dom p holds b1 /. i = (p /. i) * a ) & dom b2 = dom p & ( for i being set st i in dom p holds b2 /. i = (p /. i) * a ) holds b1 = b2 proof let it1, it2 be FinSequence of the carrier of L; ::_thesis: ( dom it1 = dom p & ( for i being set st i in dom p holds it1 /. i = (p /. i) * a ) & dom it2 = dom p & ( for i being set st i in dom p holds it2 /. i = (p /. i) * a ) implies it1 = it2 ) assume that A4: dom it1 = dom p and A5: for i being set st i in dom p holds it1 /. i = (p /. i) * a and A6: dom it2 = dom p and A7: for i being set st i in dom p holds it2 /. i = (p /. i) * a ; ::_thesis: it1 = it2 now__::_thesis:_for_j_being_Nat_st_j_in_dom_p_holds_ it1_/._j_=_it2_/._j let j be Nat; ::_thesis: ( j in dom p implies it1 /. j = it2 /. j ) assume A8: j in dom p ; ::_thesis: it1 /. j = it2 /. j hence it1 /. j = (p /. j) * a by A5 .= it2 /. j by A7, A8 ; ::_thesis: verum end; hence it1 = it2 by A4, A6, FINSEQ_5:12; ::_thesis: verum end; end; :: deftheorem Def2 defines * POLYNOM1:def_2_:_ for L being non empty multMagma for p being FinSequence of the carrier of L for a being Element of L for b4 being FinSequence of the carrier of L holds ( b4 = p * a iff ( dom b4 = dom p & ( for i being set st i in dom p holds b4 /. i = (p /. i) * a ) ) ); theorem Th6: :: POLYNOM1:6 for L being non empty multMagma for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L proof let L be non empty multMagma ; ::_thesis: for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L let a be Element of L; ::_thesis: a * (<*> the carrier of L) = <*> the carrier of L dom (a * (<*> the carrier of L)) = dom (<*> the carrier of L) by Def1; hence a * (<*> the carrier of L) = <*> the carrier of L ; ::_thesis: verum end; theorem Th7: :: POLYNOM1:7 for L being non empty multMagma for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L proof let L be non empty multMagma ; ::_thesis: for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L let a be Element of L; ::_thesis: (<*> the carrier of L) * a = <*> the carrier of L dom ((<*> the carrier of L) * a) = dom (<*> the carrier of L) by Def2; hence (<*> the carrier of L) * a = <*> the carrier of L ; ::_thesis: verum end; theorem Th8: :: POLYNOM1:8 for L being non empty multMagma for a, b being Element of L holds a * <*b*> = <*(a * b)*> proof let L be non empty multMagma ; ::_thesis: for a, b being Element of L holds a * <*b*> = <*(a * b)*> let a, b be Element of L; ::_thesis: a * <*b*> = <*(a * b)*> A1: for i being set st i in dom <*b*> holds <*(a * b)*> /. i = a * (<*b*> /. i) proof let i be set ; ::_thesis: ( i in dom <*b*> implies <*(a * b)*> /. i = a * (<*b*> /. i) ) assume i in dom <*b*> ; ::_thesis: <*(a * b)*> /. i = a * (<*b*> /. i) then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then A2: i = 1 by TARSKI:def_1; hence <*(a * b)*> /. i = a * b by FINSEQ_4:16 .= a * (<*b*> /. i) by A2, FINSEQ_4:16 ; ::_thesis: verum end; dom <*(a * b)*> = Seg 1 by FINSEQ_1:38 .= dom <*b*> by FINSEQ_1:38 ; hence a * <*b*> = <*(a * b)*> by A1, Def1; ::_thesis: verum end; theorem Th9: :: POLYNOM1:9 for L being non empty multMagma for a, b being Element of L holds <*b*> * a = <*(b * a)*> proof let L be non empty multMagma ; ::_thesis: for a, b being Element of L holds <*b*> * a = <*(b * a)*> let a, b be Element of L; ::_thesis: <*b*> * a = <*(b * a)*> A1: for i being set st i in dom <*b*> holds <*(b * a)*> /. i = (<*b*> /. i) * a proof let i be set ; ::_thesis: ( i in dom <*b*> implies <*(b * a)*> /. i = (<*b*> /. i) * a ) assume i in dom <*b*> ; ::_thesis: <*(b * a)*> /. i = (<*b*> /. i) * a then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then A2: i = 1 by TARSKI:def_1; hence <*(b * a)*> /. i = b * a by FINSEQ_4:16 .= (<*b*> /. i) * a by A2, FINSEQ_4:16 ; ::_thesis: verum end; dom <*(b * a)*> = Seg 1 by FINSEQ_1:38 .= dom <*b*> by FINSEQ_1:38 ; hence <*b*> * a = <*(b * a)*> by A1, Def2; ::_thesis: verum end; theorem Th10: :: POLYNOM1:10 for L being non empty multMagma for a being Element of L for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q) proof let L be non empty multMagma ; ::_thesis: for a being Element of L for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q) let a be Element of L; ::_thesis: for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q) let p, q be FinSequence of the carrier of L; ::_thesis: a * (p ^ q) = (a * p) ^ (a * q) A1: dom (a * (p ^ q)) = dom (p ^ q) by Def1; A2: dom (a * q) = dom q by Def1; then A3: len (a * q) = len q by FINSEQ_3:29; A4: dom (a * p) = dom p by Def1; then A5: len (a * p) = len p by FINSEQ_3:29; A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(a_*_(p_^_q))_holds_ (a_*_(p_^_q))_/._i_=_((a_*_p)_^_(a_*_q))_/._i let i be Nat; ::_thesis: ( i in dom (a * (p ^ q)) implies (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1 ) assume A7: i in dom (a * (p ^ q)) ; ::_thesis: (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1 percases ( i in dom p or ex n being Nat st ( n in dom q & i = (len p) + n ) ) by A1, A7, FINSEQ_1:25; supposeA8: i in dom p ; ::_thesis: (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1 thus (a * (p ^ q)) /. i = a * ((p ^ q) /. i) by A1, A7, Def1 .= a * (p /. i) by A8, FINSEQ_4:68 .= (a * p) /. i by A8, Def1 .= ((a * p) ^ (a * q)) /. i by A4, A8, FINSEQ_4:68 ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom q & i = (len p) + n ) ; ::_thesis: (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1 then consider n being Nat such that A9: n in dom q and A10: i = (len p) + n ; thus (a * (p ^ q)) /. i = a * ((p ^ q) /. i) by A1, A7, Def1 .= a * (q /. n) by A9, A10, FINSEQ_4:69 .= (a * q) /. n by A9, Def1 .= ((a * p) ^ (a * q)) /. i by A5, A2, A9, A10, FINSEQ_4:69 ; ::_thesis: verum end; end; end; len ((a * p) ^ (a * q)) = (len (a * p)) + (len (a * q)) by FINSEQ_1:22 .= len (p ^ q) by A5, A3, FINSEQ_1:22 ; then dom (a * (p ^ q)) = dom ((a * p) ^ (a * q)) by A1, FINSEQ_3:29; hence a * (p ^ q) = (a * p) ^ (a * q) by A6, FINSEQ_5:12; ::_thesis: verum end; theorem Th11: :: POLYNOM1:11 for L being non empty multMagma for a being Element of L for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a) proof let L be non empty multMagma ; ::_thesis: for a being Element of L for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a) let a be Element of L; ::_thesis: for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a) let p, q be FinSequence of the carrier of L; ::_thesis: (p ^ q) * a = (p * a) ^ (q * a) A1: dom ((p ^ q) * a) = dom (p ^ q) by Def2; A2: dom (q * a) = dom q by Def2; then A3: len (q * a) = len q by FINSEQ_3:29; A4: dom (p * a) = dom p by Def2; then A5: len (p * a) = len p by FINSEQ_3:29; A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_((p_^_q)_*_a)_holds_ ((p_^_q)_*_a)_/._i_=_((p_*_a)_^_(q_*_a))_/._i let i be Nat; ::_thesis: ( i in dom ((p ^ q) * a) implies ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1 ) assume A7: i in dom ((p ^ q) * a) ; ::_thesis: ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1 percases ( i in dom p or ex n being Nat st ( n in dom q & i = (len p) + n ) ) by A1, A7, FINSEQ_1:25; supposeA8: i in dom p ; ::_thesis: ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1 thus ((p ^ q) * a) /. i = ((p ^ q) /. i) * a by A1, A7, Def2 .= (p /. i) * a by A8, FINSEQ_4:68 .= (p * a) /. i by A8, Def2 .= ((p * a) ^ (q * a)) /. i by A4, A8, FINSEQ_4:68 ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom q & i = (len p) + n ) ; ::_thesis: ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1 then consider n being Nat such that A9: n in dom q and A10: i = (len p) + n ; thus ((p ^ q) * a) /. i = ((p ^ q) /. i) * a by A1, A7, Def2 .= (q /. n) * a by A9, A10, FINSEQ_4:69 .= (q * a) /. n by A9, Def2 .= ((p * a) ^ (q * a)) /. i by A5, A2, A9, A10, FINSEQ_4:69 ; ::_thesis: verum end; end; end; len ((p * a) ^ (q * a)) = (len (p * a)) + (len (q * a)) by FINSEQ_1:22 .= len (p ^ q) by A5, A3, FINSEQ_1:22 ; then dom ((p ^ q) * a) = dom ((p * a) ^ (q * a)) by A1, FINSEQ_3:29; hence (p ^ q) * a = (p * a) ^ (q * a) by A6, FINSEQ_5:12; ::_thesis: verum end; registration cluster non empty strict right_unital for multLoopStr_0 ; existence ex b1 being non empty strict multLoopStr_0 st b1 is right_unital proof take multEX_0 ; ::_thesis: multEX_0 is right_unital thus multEX_0 is right_unital ; ::_thesis: verum end; end; registration cluster non empty non trivial right_complementable almost_left_invertible strict associative commutative well-unital distributive Abelian add-associative right_zeroed for doubleLoopStr ; existence ex b1 being non empty doubleLoopStr st ( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is distributive & b1 is almost_left_invertible & b1 is well-unital & not b1 is trivial ) proof take F_Real ; ::_thesis: ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is associative & F_Real is commutative & F_Real is distributive & F_Real is almost_left_invertible & F_Real is well-unital & not F_Real is trivial ) thus ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is associative & F_Real is commutative & F_Real is distributive & F_Real is almost_left_invertible & F_Real is well-unital & not F_Real is trivial ) ; ::_thesis: verum end; end; theorem Th12: :: POLYNOM1:12 for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr for a being Element of L for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p) proof let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p) let a be Element of L; ::_thesis: for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p) set p = <*> the carrier of L; defpred S1[ FinSequence of the carrier of L] means Sum (a * $1) = a * (Sum $1); A1: now__::_thesis:_for_p_being_FinSequence_of_the_carrier_of_L for_r_being_Element_of_L_st_S1[p]_holds_ S1[p_^_<*r*>] let p be FinSequence of the carrier of L; ::_thesis: for r being Element of L st S1[p] holds S1[p ^ <*r*>] let r be Element of L; ::_thesis: ( S1[p] implies S1[p ^ <*r*>] ) assume A2: S1[p] ; ::_thesis: S1[p ^ <*r*>] Sum (a * (p ^ <*r*>)) = Sum ((a * p) ^ (a * <*r*>)) by Th10 .= (Sum (a * p)) + (Sum (a * <*r*>)) by RLVECT_1:41 .= (Sum (a * p)) + (Sum <*(a * r)*>) by Th8 .= (Sum (a * p)) + (a * r) by RLVECT_1:44 .= (a * (Sum p)) + (a * (Sum <*r*>)) by A2, RLVECT_1:44 .= a * ((Sum p) + (Sum <*r*>)) by VECTSP_1:def_7 .= a * (Sum (p ^ <*r*>)) by RLVECT_1:41 ; hence S1[p ^ <*r*>] ; ::_thesis: verum end; ( Sum (<*> the carrier of L) = 0. L & Sum (a * (<*> the carrier of L)) = Sum (<*> the carrier of L) ) by Th6, RLVECT_1:43; then A3: S1[ <*> the carrier of L] by VECTSP_1:6; thus for p being FinSequence of the carrier of L holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum end; theorem Th13: :: POLYNOM1:13 for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr for a being Element of L for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a proof let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a let a be Element of L; ::_thesis: for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a set p = <*> the carrier of L; defpred S1[ FinSequence of the carrier of L] means Sum ($1 * a) = (Sum $1) * a; A1: now__::_thesis:_for_p_being_FinSequence_of_the_carrier_of_L for_r_being_Element_of_L_st_S1[p]_holds_ S1[p_^_<*r*>] let p be FinSequence of the carrier of L; ::_thesis: for r being Element of L st S1[p] holds S1[p ^ <*r*>] let r be Element of L; ::_thesis: ( S1[p] implies S1[p ^ <*r*>] ) assume A2: S1[p] ; ::_thesis: S1[p ^ <*r*>] Sum ((p ^ <*r*>) * a) = Sum ((p * a) ^ (<*r*> * a)) by Th11 .= (Sum (p * a)) + (Sum (<*r*> * a)) by RLVECT_1:41 .= (Sum (p * a)) + (Sum <*(r * a)*>) by Th9 .= (Sum (p * a)) + (r * a) by RLVECT_1:44 .= ((Sum p) * a) + ((Sum <*r*>) * a) by A2, RLVECT_1:44 .= ((Sum p) + (Sum <*r*>)) * a by VECTSP_1:def_7 .= (Sum (p ^ <*r*>)) * a by RLVECT_1:41 ; hence S1[p ^ <*r*>] ; ::_thesis: verum end; ( Sum (<*> the carrier of L) = 0. L & Sum ((<*> the carrier of L) * a) = Sum (<*> the carrier of L) ) by Th7, RLVECT_1:43; then A3: S1[ <*> the carrier of L] by VECTSP_1:7; thus for p being FinSequence of the carrier of L holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum end; begin theorem Th14: :: POLYNOM1:14 for L being non empty right_complementable add-associative right_zeroed addLoopStr for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F) proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F) defpred S1[ FinSequence of the carrier of L * ] means Sum (FlattenSeq $1) = Sum (Sum $1); A1: for f being FinSequence of the carrier of L * for p being Element of the carrier of L * st S1[f] holds S1[f ^ <*p*>] proof let f be FinSequence of the carrier of L * ; ::_thesis: for p being Element of the carrier of L * st S1[f] holds S1[f ^ <*p*>] let p be Element of the carrier of L * ; ::_thesis: ( S1[f] implies S1[f ^ <*p*>] ) assume A2: Sum (FlattenSeq f) = Sum (Sum f) ; ::_thesis: S1[f ^ <*p*>] thus Sum (FlattenSeq (f ^ <*p*>)) = Sum ((FlattenSeq f) ^ (FlattenSeq <*p*>)) by PRE_POLY:3 .= Sum ((FlattenSeq f) ^ p) by PRE_POLY:1 .= (Sum (Sum f)) + (Sum p) by A2, RLVECT_1:41 .= (Sum (Sum f)) + (Sum <*(Sum p)*>) by RLVECT_1:44 .= Sum ((Sum f) ^ <*(Sum p)*>) by RLVECT_1:41 .= Sum ((Sum f) ^ (Sum <*p*>)) by Th4 .= Sum (Sum (f ^ <*p*>)) by Th5 ; ::_thesis: verum end; Sum (FlattenSeq (<*> ( the carrier of L *))) = Sum (<*> the carrier of L) ; then A3: S1[ <*> ( the carrier of L *)] by Th3; thus for f being FinSequence of the carrier of L * holds S1[f] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum end; definition let X be non empty set ; let S be ZeroStr ; let f be Function of X,S; func Support f -> Subset of X means :Def3: :: POLYNOM1:def 3 for x being Element of X holds ( x in it iff f . x <> 0. S ); existence ex b1 being Subset of X st for x being Element of X holds ( x in b1 iff f . x <> 0. S ) proof defpred S1[ set ] means f . $1 <> 0. S; consider B being Subset of X such that A1: for x being Element of X holds ( x in B iff S1[x] ) from SUBSET_1:sch_3(); take B ; ::_thesis: for x being Element of X holds ( x in B iff f . x <> 0. S ) thus for x being Element of X holds ( x in B iff f . x <> 0. S ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of X st ( for x being Element of X holds ( x in b1 iff f . x <> 0. S ) ) & ( for x being Element of X holds ( x in b2 iff f . x <> 0. S ) ) holds b1 = b2 proof let A, B be Subset of X; ::_thesis: ( ( for x being Element of X holds ( x in A iff f . x <> 0. S ) ) & ( for x being Element of X holds ( x in B iff f . x <> 0. S ) ) implies A = B ) assume that A2: for x being Element of X holds ( x in A iff f . x <> 0. S ) and A3: for x being Element of X holds ( x in B iff f . x <> 0. S ) ; ::_thesis: A = B now__::_thesis:_for_x_being_Element_of_X_holds_ (_x_in_A_iff_x_in_B_) let x be Element of X; ::_thesis: ( x in A iff x in B ) ( x in A iff f . x <> 0. S ) by A2; hence ( x in A iff x in B ) by A3; ::_thesis: verum end; hence A = B by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def3 defines Support POLYNOM1:def_3_:_ for X being non empty set for S being ZeroStr for f being Function of X,S for b4 being Subset of X holds ( b4 = Support f iff for x being Element of X holds ( x in b4 iff f . x <> 0. S ) ); definition let X be non empty set ; let S be ZeroStr ; let p be Function of X,S; attrp is finite-Support means :Def4: :: POLYNOM1:def 4 Support p is finite ; end; :: deftheorem Def4 defines finite-Support POLYNOM1:def_4_:_ for X being non empty set for S being ZeroStr for p being Function of X,S holds ( p is finite-Support iff Support p is finite ); definition let n be set ; let L be non empty 1-sorted ; let p be Function of (Bags n),L; let x be bag of n; :: original: . redefine funcp . x -> Element of L; coherence p . x is Element of L proof reconsider b = x as Element of Bags n by PRE_POLY:def_12; reconsider f = p as Function of (Bags n), the carrier of L ; f . b is Element of L ; hence p . x is Element of L ; ::_thesis: verum end; end; begin definition let X be set ; let S be 1-sorted ; mode Series of X,S is Function of (Bags X),S; end; definition let n be set ; let L be non empty addLoopStr ; let p, q be Series of n,L; funcp + q -> Series of n,L equals :: POLYNOM1:def 5 p + q; coherence p + q is Series of n,L ; end; :: deftheorem defines + POLYNOM1:def_5_:_ for n being set for L being non empty addLoopStr for p, q being Series of n,L holds p + q = p + q; theorem Th15: :: POLYNOM1:15 for n being set for L being non empty addLoopStr for p, q being Series of n,L for x being bag of n holds (p + q) . x = (p . x) + (q . x) proof let n be set ; ::_thesis: for L being non empty addLoopStr for p, q being Series of n,L for x being bag of n holds (p + q) . x = (p . x) + (q . x) let L be non empty addLoopStr ; ::_thesis: for p, q being Series of n,L for x being bag of n holds (p + q) . x = (p . x) + (q . x) let p, q be Series of n,L; ::_thesis: for x being bag of n holds (p + q) . x = (p . x) + (q . x) let x be bag of n; ::_thesis: (p + q) . x = (p . x) + (q . x) A1: ( dom p = Bags n & dom q = Bags n ) by FUNCT_2:def_1; A2: x in Bags n by PRE_POLY:def_12; then A3: ( p /. x = p . x & q /. x = q . x ) by A1, PARTFUN1:def_6; A4: dom (p + q) = (dom p) /\ (dom q) by VFUNCT_1:def_1; hence (p + q) . x = (p + q) /. x by A1, A2, PARTFUN1:def_6 .= (p . x) + (q . x) by A1, A2, A3, A4, VFUNCT_1:def_1 ; ::_thesis: verum end; theorem :: POLYNOM1:16 for n being set for L being non empty addLoopStr for p, q, r being Series of n,L st ( for x being bag of n holds r . x = (p . x) + (q . x) ) holds r = p + q proof let n be set ; ::_thesis: for L being non empty addLoopStr for p, q, r being Series of n,L st ( for x being bag of n holds r . x = (p . x) + (q . x) ) holds r = p + q let L be non empty addLoopStr ; ::_thesis: for p, q, r being Series of n,L st ( for x being bag of n holds r . x = (p . x) + (q . x) ) holds r = p + q let p, q, r be Series of n,L; ::_thesis: ( ( for x being bag of n holds r . x = (p . x) + (q . x) ) implies r = p + q ) assume A1: for x being bag of n holds r . x = (p . x) + (q . x) ; ::_thesis: r = p + q let x be Element of Bags n; :: according to FUNCT_2:def_8 ::_thesis: r . x = (p + q) . x A2: dom (p + q) = Bags n by FUNCT_2:def_1; A3: (p + q) /. x = (p + q) . x ; A4: ( p /. x = p . x & q /. x = q . x ) ; thus r . x = (p . x) + (q . x) by A1 .= (p + q) . x by A2, A3, A4, VFUNCT_1:def_1 ; ::_thesis: verum end; theorem Th17: :: POLYNOM1:17 for n being set for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Series of n,L for x being bag of n holds (- p) . x = - (p . x) proof let n be set ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Series of n,L for x being bag of n holds (- p) . x = - (p . x) let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L for x being bag of n holds (- p) . x = - (p . x) let p be Series of n,L; ::_thesis: for x being bag of n holds (- p) . x = - (p . x) let x be bag of n; ::_thesis: (- p) . x = - (p . x) A1: dom p = Bags n by FUNCT_2:def_1; A2: x in Bags n by PRE_POLY:def_12; then A3: p /. x = p . x by A1, PARTFUN1:def_6; A4: dom (- p) = dom p by VFUNCT_1:def_5; hence (- p) . x = (- p) /. x by A1, A2, PARTFUN1:def_6 .= - (p . x) by A1, A2, A3, A4, VFUNCT_1:def_5 ; ::_thesis: verum end; theorem :: POLYNOM1:18 for n being set for L being non empty right_complementable add-associative right_zeroed addLoopStr for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds r = - p proof let n be set ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds r = - p let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds r = - p let p, r be Series of n,L; ::_thesis: ( ( for x being bag of n holds r . x = - (p . x) ) implies r = - p ) assume A1: for x being bag of n holds r . x = - (p . x) ; ::_thesis: r = - p let x be Element of Bags n; :: according to FUNCT_2:def_8 ::_thesis: r . x = (- p) . x A2: dom (- p) = Bags n by FUNCT_2:def_1; A3: (- p) /. x = (- p) . x ; A4: p /. x = p . x ; thus r . x = - (p . x) by A1 .= (- p) . x by A2, A3, A4, VFUNCT_1:def_5 ; ::_thesis: verum end; theorem :: POLYNOM1:19 for n being set for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Series of n,L holds p = - (- p) proof let n be set ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Series of n,L holds p = - (- p) let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L holds p = - (- p) let p be Series of n,L; ::_thesis: p = - (- p) set r = - p; A1: dom p = Bags n by FUNCT_2:def_1; A2: dom (- p) = Bags n by FUNCT_2:def_1; A3: dom (- p) = dom p by VFUNCT_1:def_5; A4: dom (- (- p)) = dom (- p) by VFUNCT_1:def_5; A5: dom (- (- p)) = dom (- p) by VFUNCT_1:def_5; now__::_thesis:_for_x_being_Element_of_Bags_n_st_x_in_dom_p_holds_ p_._x_=_(-_(-_p))_._x let x be Element of Bags n; ::_thesis: ( x in dom p implies p . x = (- (- p)) . x ) assume x in dom p ; ::_thesis: p . x = (- (- p)) . x A6: p . x = p /. x ; thus p . x = - (- (p . x)) by RLVECT_1:17 .= - ((- p) /. x) by A1, A3, A6, VFUNCT_1:def_5 .= (- (- p)) /. x by A1, A3, A5, VFUNCT_1:def_5 .= (- (- p)) . x ; ::_thesis: verum end; hence p = - (- p) by A1, A2, A4, PARTFUN1:5; ::_thesis: verum end; theorem Th20: :: POLYNOM1:20 for n being set for L being non empty right_zeroed addLoopStr for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q) proof let n be set ; ::_thesis: for L being non empty right_zeroed addLoopStr for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q) let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q) let p, q be Series of n,L; ::_thesis: Support (p + q) c= (Support p) \/ (Support q) set f = p + q; set Sp = Support p; set Sq = Support q; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support (p + q) or x in (Support p) \/ (Support q) ) assume A1: x in Support (p + q) ; ::_thesis: x in (Support p) \/ (Support q) then reconsider x9 = x as Element of Bags n ; (p + q) . x9 <> 0. L by A1, Def3; then (p . x9) + (q . x9) <> 0. L by Th15; then ( not p . x9 = 0. L or not q . x9 = 0. L ) by RLVECT_1:def_4; then ( x9 in Support p or x9 in Support q ) by Def3; hence x in (Support p) \/ (Support q) by XBOOLE_0:def_3; ::_thesis: verum end; definition let n be set ; let L be non empty Abelian right_zeroed addLoopStr ; let p, q be Series of n,L; :: original: + redefine funcp + q -> Series of n,L; commutativity for p, q being Series of n,L holds p + q = q + p proof let p, q be Series of n,L; ::_thesis: p + q = q + p now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_+_q)_._b_=_(q_+_p)_._b let b be Element of Bags n; ::_thesis: (p + q) . b = (q + p) . b thus (p + q) . b = (q . b) + (p . b) by Th15 .= (q + p) . b by Th15 ; ::_thesis: verum end; hence p + q = q + p by FUNCT_2:63; ::_thesis: verum end; end; theorem Th21: :: POLYNOM1:21 for n being set for L being non empty add-associative right_zeroed doubleLoopStr for p, q, r being Series of n,L holds (p + q) + r = p + (q + r) proof let n be set ; ::_thesis: for L being non empty add-associative right_zeroed doubleLoopStr for p, q, r being Series of n,L holds (p + q) + r = p + (q + r) let L be non empty add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Series of n,L holds (p + q) + r = p + (q + r) let p, q, r be Series of n,L; ::_thesis: (p + q) + r = p + (q + r) now__::_thesis:_for_b_being_Element_of_Bags_n_holds_((p_+_q)_+_r)_._b_=_(p_+_(q_+_r))_._b let b be Element of Bags n; ::_thesis: ((p + q) + r) . b = (p + (q + r)) . b thus ((p + q) + r) . b = ((p + q) . b) + (r . b) by Th15 .= ((p . b) + (q . b)) + (r . b) by Th15 .= (p . b) + ((q . b) + (r . b)) by RLVECT_1:def_3 .= (p . b) + ((q + r) . b) by Th15 .= (p + (q + r)) . b by Th15 ; ::_thesis: verum end; hence (p + q) + r = p + (q + r) by FUNCT_2:63; ::_thesis: verum end; definition let n be set ; let L be non empty right_complementable add-associative right_zeroed addLoopStr ; let p, q be Series of n,L; funcp - q -> Series of n,L equals :: POLYNOM1:def 6 p + (- q); coherence p + (- q) is Series of n,L ; end; :: deftheorem defines - POLYNOM1:def_6_:_ for n being set for L being non empty right_complementable add-associative right_zeroed addLoopStr for p, q being Series of n,L holds p - q = p + (- q); definition let n be set ; let S be non empty ZeroStr ; func 0_ (n,S) -> Series of n,S equals :: POLYNOM1:def 7 (Bags n) --> (0. S); coherence (Bags n) --> (0. S) is Series of n,S ; end; :: deftheorem defines 0_ POLYNOM1:def_7_:_ for n being set for S being non empty ZeroStr holds 0_ (n,S) = (Bags n) --> (0. S); theorem Th22: :: POLYNOM1:22 for n being set for S being non empty ZeroStr for b being bag of n holds (0_ (n,S)) . b = 0. S proof let n be set ; ::_thesis: for S being non empty ZeroStr for b being bag of n holds (0_ (n,S)) . b = 0. S let S be non empty ZeroStr ; ::_thesis: for b being bag of n holds (0_ (n,S)) . b = 0. S let b be bag of n; ::_thesis: (0_ (n,S)) . b = 0. S b in Bags n by PRE_POLY:def_12; hence (0_ (n,S)) . b = 0. S by FUNCOP_1:7; ::_thesis: verum end; theorem Th23: :: POLYNOM1:23 for n being set for L being non empty right_zeroed addLoopStr for p being Series of n,L holds p + (0_ (n,L)) = p proof let n be set ; ::_thesis: for L being non empty right_zeroed addLoopStr for p being Series of n,L holds p + (0_ (n,L)) = p let L be non empty right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L holds p + (0_ (n,L)) = p let p be Series of n,L; ::_thesis: p + (0_ (n,L)) = p reconsider ls = p + (0_ (n,L)), p9 = p as Function of (Bags n), the carrier of L ; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_ls_._b_=_p9_._b let b be Element of Bags n; ::_thesis: ls . b = p9 . b thus ls . b = (p . b) + ((0_ (n,L)) . b) by Th15 .= (p9 . b) + (0. L) by Th22 .= p9 . b by RLVECT_1:def_4 ; ::_thesis: verum end; hence p + (0_ (n,L)) = p by FUNCT_2:63; ::_thesis: verum end; definition let n be set ; let L be non empty right_unital multLoopStr_0 ; func 1_ (n,L) -> Series of n,L equals :: POLYNOM1:def 8 (0_ (n,L)) +* ((EmptyBag n),(1. L)); coherence (0_ (n,L)) +* ((EmptyBag n),(1. L)) is Series of n,L ; end; :: deftheorem defines 1_ POLYNOM1:def_8_:_ for n being set for L being non empty right_unital multLoopStr_0 holds 1_ (n,L) = (0_ (n,L)) +* ((EmptyBag n),(1. L)); theorem Th24: :: POLYNOM1:24 for n being set for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Series of n,L holds p - p = 0_ (n,L) proof let n be set ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Series of n,L holds p - p = 0_ (n,L) let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L holds p - p = 0_ (n,L) let p be Series of n,L; ::_thesis: p - p = 0_ (n,L) reconsider pp = p - p, Z = 0_ (n,L) as Function of (Bags n), the carrier of L ; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_pp_._b_=_Z_._b let b be Element of Bags n; ::_thesis: pp . b = Z . b thus pp . b = (p . b) + ((- p) . b) by Th15 .= (p . b) + (- (p . b)) by Th17 .= 0. L by RLVECT_1:def_10 .= Z . b by Th22 ; ::_thesis: verum end; hence p - p = 0_ (n,L) by FUNCT_2:63; ::_thesis: verum end; theorem Th25: :: POLYNOM1:25 for n being set for L being non empty right_unital multLoopStr_0 holds ( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds (1_ (n,L)) . b = 0. L ) ) proof let n be set ; ::_thesis: for L being non empty right_unital multLoopStr_0 holds ( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds (1_ (n,L)) . b = 0. L ) ) let L be non empty right_unital multLoopStr_0 ; ::_thesis: ( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds (1_ (n,L)) . b = 0. L ) ) set Z = 0_ (n,L); dom (0_ (n,L)) = Bags n by FUNCOP_1:13; hence (1_ (n,L)) . (EmptyBag n) = 1. L by FUNCT_7:31; ::_thesis: for b being bag of n st b <> EmptyBag n holds (1_ (n,L)) . b = 0. L let b be bag of n; ::_thesis: ( b <> EmptyBag n implies (1_ (n,L)) . b = 0. L ) A1: b in Bags n by PRE_POLY:def_12; assume b <> EmptyBag n ; ::_thesis: (1_ (n,L)) . b = 0. L hence (1_ (n,L)) . b = (0_ (n,L)) . b by FUNCT_7:32 .= 0. L by A1, FUNCOP_1:7 ; ::_thesis: verum end; definition let n be Ordinal; let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ; let p, q be Series of n,L; funcp *' q -> Series of n,L means :Def9: :: POLYNOM1:def 9 for b being bag of n ex s being FinSequence of the carrier of L st ( it . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ); existence ex b1 being Series of n,L st for b being bag of n ex s being FinSequence of the carrier of L st ( b1 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) proof defpred S1[ Element of Bags n, Element of L] means ex b being bag of n st ( b = $1 & ex s being FinSequence of the carrier of L st ( $2 = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ); A1: now__::_thesis:_for_bb_being_Element_of_Bags_n_ex_y_being_Element_of_L_st_S1[bb,y] let bb be Element of Bags n; ::_thesis: ex y being Element of L st S1[bb,y] reconsider b = bb as bag of n ; defpred S2[ Nat, set ] means ex b1, b2 being bag of n st ( (decomp b) /. $1 = <*b1,b2*> & $2 = (p . b1) * (q . b2) ); A2: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(len_(decomp_b))_holds_ ex_x_being_Element_of_L_st_S2[k,x] let k be Nat; ::_thesis: ( k in Seg (len (decomp b)) implies ex x being Element of L st S2[k,x] ) assume k in Seg (len (decomp b)) ; ::_thesis: ex x being Element of L st S2[k,x] then k in dom (decomp b) by FINSEQ_1:def_3; then consider b1, b2 being bag of n such that A3: (decomp b) /. k = <*b1,b2*> and b = b1 + b2 by PRE_POLY:68; reconsider x = (p . b1) * (q . b2) as Element of L ; take x = x; ::_thesis: S2[k,x] thus S2[k,x] by A3; ::_thesis: verum end; consider s being FinSequence of the carrier of L such that A4: len s = len (decomp b) and A5: for k being Nat st k in Seg (len (decomp b)) holds S2[k,s /. k] from FINSEQ_4:sch_1(A2); reconsider y = Sum s as Element of L ; take y = y; ::_thesis: S1[bb,y] thus S1[bb,y] ::_thesis: verum proof take b ; ::_thesis: ( b = bb & ex s being FinSequence of the carrier of L st ( y = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) thus b = bb ; ::_thesis: ex s being FinSequence of the carrier of L st ( y = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) take s ; ::_thesis: ( y = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) thus y = Sum s ; ::_thesis: ( len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) thus len s = len (decomp b) by A4; ::_thesis: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) let k be Element of NAT ; ::_thesis: ( k in dom s implies ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) assume k in dom s ; ::_thesis: ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) then k in Seg (len (decomp b)) by A4, FINSEQ_1:def_3; hence ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by A5; ::_thesis: verum end; end; consider P being Function of (Bags n), the carrier of L such that A6: for b being Element of Bags n holds S1[b,P . b] from FUNCT_2:sch_3(A1); reconsider P = P as Function of (Bags n),L ; reconsider P = P as Series of n,L ; take P ; ::_thesis: for b being bag of n ex s being FinSequence of the carrier of L st ( P . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) let b be bag of n; ::_thesis: ex s being FinSequence of the carrier of L st ( P . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) reconsider bb = b as Element of Bags n by PRE_POLY:def_12; S1[bb,P . bb] by A6; hence ex s being FinSequence of the carrier of L st ( P . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Series of n,L st ( for b being bag of n ex s being FinSequence of the carrier of L st ( b1 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st ( b2 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) holds b1 = b2 proof let it1, it2 be Series of n,L; ::_thesis: ( ( for b being bag of n ex s being FinSequence of the carrier of L st ( it1 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st ( it2 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) implies it1 = it2 ) assume that A7: for b being bag of n ex s being FinSequence of the carrier of L st ( it1 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) and A8: for b being bag of n ex s being FinSequence of the carrier of L st ( it2 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ; ::_thesis: it1 = it2 reconsider ita = it1, itb = it2 as Function of (Bags n), the carrier of L ; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_ita_._b_=_itb_._b let b be Element of Bags n; ::_thesis: ita . b = itb . b consider sa being FinSequence of the carrier of L such that A9: ita . b = Sum sa and A10: len sa = len (decomp b) and A11: for k being Element of NAT st k in dom sa holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & sa /. k = (p . b1) * (q . b2) ) by A7; consider sb being FinSequence of the carrier of L such that A12: itb . b = Sum sb and A13: len sb = len (decomp b) and A14: for k being Element of NAT st k in dom sb holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & sb /. k = (p . b1) * (q . b2) ) by A8; now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_sa_holds_ sa_._k_=_sb_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len sa implies sa . k = sb . k ) assume A15: ( 1 <= k & k <= len sa ) ; ::_thesis: sa . k = sb . k then A16: k in dom sa by FINSEQ_3:25; then A17: sa /. k = sa . k by PARTFUN1:def_6; A18: k in dom sb by A10, A13, A15, FINSEQ_3:25; then A19: sb /. k = sb . k by PARTFUN1:def_6; consider ab1, ab2 being bag of n such that A20: (decomp b) /. k = <*ab1,ab2*> and A21: sa /. k = (p . ab1) * (q . ab2) by A11, A16; consider bb1, bb2 being bag of n such that A22: (decomp b) /. k = <*bb1,bb2*> and A23: sb /. k = (p . bb1) * (q . bb2) by A14, A18; ab1 = bb1 by A20, A22, FINSEQ_1:77; hence sa . k = sb . k by A20, A21, A22, A23, A17, A19, FINSEQ_1:77; ::_thesis: verum end; hence ita . b = itb . b by A9, A10, A12, A13, FINSEQ_1:14; ::_thesis: verum end; hence it1 = it2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def9 defines *' POLYNOM1:def_9_:_ for n being Ordinal for L being non empty right_complementable add-associative right_zeroed doubleLoopStr for p, q, b5 being Series of n,L holds ( b5 = p *' q iff for b being bag of n ex s being FinSequence of the carrier of L st ( b5 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ); theorem Th26: :: POLYNOM1:26 for n being Ordinal for L being non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r) proof let n be Ordinal; ::_thesis: for L being non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r) let L be non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r) let p, q, r be Series of n,L; ::_thesis: p *' (q + r) = (p *' q) + (p *' r) set cL = the carrier of L; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_*'_(q_+_r))_._b_=_((p_*'_q)_+_(p_*'_r))_._b let b be Element of Bags n; ::_thesis: (p *' (q + r)) . b = ((p *' q) + (p *' r)) . b consider s being FinSequence of the carrier of L such that A1: (p *' (q + r)) . b = Sum s and A2: len s = len (decomp b) and A3: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((q + r) . b2) ) by Def9; consider u being FinSequence of the carrier of L such that A4: (p *' r) . b = Sum u and A5: len u = len (decomp b) and A6: for k being Element of NAT st k in dom u holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & u /. k = (p . b1) * (r . b2) ) by Def9; consider t being FinSequence of the carrier of L such that A7: (p *' q) . b = Sum t and A8: len t = len (decomp b) and A9: for k being Element of NAT st k in dom t holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & t /. k = (p . b1) * (q . b2) ) by Def9; reconsider t = t, u = u as Element of (len s) -tuples_on the carrier of L by A2, A8, A5, FINSEQ_2:92; A10: dom u = dom s by A2, A5, FINSEQ_3:29; A11: dom t = dom s by A2, A8, FINSEQ_3:29; then A12: dom (t + u) = dom s by A10, Th1; A13: now__::_thesis:_for_i_being_Nat_st_i_in_dom_s_holds_ s_._i_=_(t_+_u)_._i let i be Nat; ::_thesis: ( i in dom s implies s . i = (t + u) . i ) assume A14: i in dom s ; ::_thesis: s . i = (t + u) . i then consider sb1, sb2 being bag of n such that A15: (decomp b) /. i = <*sb1,sb2*> and A16: s /. i = (p . sb1) * ((q + r) . sb2) by A3; A17: ( t /. i = t . i & u /. i = u . i ) by A11, A10, A14, PARTFUN1:def_6; consider ub1, ub2 being bag of n such that A18: (decomp b) /. i = <*ub1,ub2*> and A19: u /. i = (p . ub1) * (r . ub2) by A6, A10, A14; A20: ( sb1 = ub1 & sb2 = ub2 ) by A15, A18, FINSEQ_1:77; consider tb1, tb2 being bag of n such that A21: (decomp b) /. i = <*tb1,tb2*> and A22: t /. i = (p . tb1) * (q . tb2) by A9, A11, A14; A23: ( sb1 = tb1 & sb2 = tb2 ) by A15, A21, FINSEQ_1:77; s /. i = s . i by A14, PARTFUN1:def_6; hence s . i = (p . sb1) * ((q . sb2) + (r . sb2)) by A16, Th15 .= ((p . sb1) * (q . sb2)) + ((p . sb1) * (r . sb2)) by VECTSP_1:def_7 .= (t + u) . i by A12, A14, A22, A19, A23, A20, A17, FVSUM_1:17 ; ::_thesis: verum end; len (t + u) = len s by A12, FINSEQ_3:29; then s = t + u by A13, FINSEQ_2:9; hence (p *' (q + r)) . b = (Sum t) + (Sum u) by A1, FVSUM_1:76 .= ((p *' q) + (p *' r)) . b by A7, A4, Th15 ; ::_thesis: verum end; hence p *' (q + r) = (p *' q) + (p *' r) by FUNCT_2:63; ::_thesis: verum end; theorem Th27: :: POLYNOM1:27 for n being Ordinal for L being non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r) proof let n be Ordinal; ::_thesis: for L being non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r) let L be non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r) let p, q, r be Series of n,L; ::_thesis: (p *' q) *' r = p *' (q *' r) set cL = the carrier of L; reconsider pqra = (p *' q) *' r, pqrb = p *' (q *' r) as Function of (Bags n), the carrier of L ; set pq = p *' q; set qr = q *' r; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_pqra_._b_=_pqrb_._b let b be Element of Bags n; ::_thesis: pqra . b = pqrb . b set db = decomp b; deffunc H1( Nat) -> set = (decomp (((decomp b) /. $1) /. 1)) ^^ ((len (decomp (((decomp b) /. $1) /. 1))) |-> <*(((decomp b) /. $1) /. 2)*>); consider dbl being FinSequence such that A1: len dbl = len (decomp b) and A2: for k being Nat st k in dom dbl holds dbl . k = H1(k) from FINSEQ_1:sch_2(); A3: rng dbl c= (3 -tuples_on (Bags n)) * proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng dbl or y in (3 -tuples_on (Bags n)) * ) assume y in rng dbl ; ::_thesis: y in (3 -tuples_on (Bags n)) * then consider k being set such that A4: k in dom dbl and A5: y = dbl . k by FUNCT_1:def_3; set dbk2 = ((decomp b) /. k) /. 2; set ddbk1 = decomp (((decomp b) /. k) /. 1); reconsider k = k as Nat by A4; set dblk = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>); A6: dom ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) = (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) by PRE_POLY:def_4 .= (dom (decomp (((decomp b) /. k) /. 1))) /\ (Seg (len (decomp (((decomp b) /. k) /. 1)))) by FUNCOP_1:13 .= (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3 .= dom (decomp (((decomp b) /. k) /. 1)) ; A7: dom (decomp (((decomp b) /. k) /. 1)) = Seg (len (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3; rng ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) c= 3 -tuples_on (Bags n) proof reconsider Gi = <*(((decomp b) /. k) /. 2)*> as Element of 1 -tuples_on (Bags n) by FINSEQ_2:98; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) or y in 3 -tuples_on (Bags n) ) assume y in rng ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) ; ::_thesis: y in 3 -tuples_on (Bags n) then consider i being set such that A8: i in dom ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) and A9: ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) . i = y by FUNCT_1:def_3; (decomp (((decomp b) /. k) /. 1)) . i in rng (decomp (((decomp b) /. k) /. 1)) by A6, A8, FUNCT_1:def_3; then reconsider Fi = (decomp (((decomp b) /. k) /. 1)) . i as Element of 2 -tuples_on (Bags n) ; reconsider i9 = i as Element of NAT by A8; ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) . i9 = <*(((decomp b) /. k) /. 2)*> by A6, A7, A8, FUNCOP_1:7; then y = Fi ^ Gi by A8, A9, PRE_POLY:def_4; hence y in 3 -tuples_on (Bags n) by FINSEQ_2:131; ::_thesis: verum end; then A10: (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) is FinSequence of 3 -tuples_on (Bags n) by FINSEQ_1:def_4; dbl . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) by A2, A4; hence y in (3 -tuples_on (Bags n)) * by A5, A10, FINSEQ_1:def_11; ::_thesis: verum end; deffunc H2( Element of 3 -tuples_on (Bags n)) -> Element of the carrier of L = ((p . ($1 /. 1)) * (q . ($1 /. 2))) * (r . ($1 /. 3)); consider v being Function of (3 -tuples_on (Bags n)), the carrier of L such that A11: for b being Element of 3 -tuples_on (Bags n) holds v . b = H2(b) from FUNCT_2:sch_4(); deffunc H3( Nat) -> set = ((len (decomp (((decomp b) /. $1) /. 2))) |-> <*(((decomp b) /. $1) /. 1)*>) ^^ (decomp (((decomp b) /. $1) /. 2)); consider dbr being FinSequence such that A12: len dbr = len (decomp b) and A13: for k being Nat st k in dom dbr holds dbr . k = H3(k) from FINSEQ_1:sch_2(); rng dbr c= (3 -tuples_on (Bags n)) * proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng dbr or y in (3 -tuples_on (Bags n)) * ) assume y in rng dbr ; ::_thesis: y in (3 -tuples_on (Bags n)) * then consider k being set such that A14: k in dom dbr and A15: y = dbr . k by FUNCT_1:def_3; reconsider k = k as Nat by A14; set ddbk1 = decomp (((decomp b) /. k) /. 2); set dbk2 = ((decomp b) /. k) /. 1; set dbrk = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)); A16: dom (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) = (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>)) by PRE_POLY:def_4 .= (dom (decomp (((decomp b) /. k) /. 2))) /\ (Seg (len (decomp (((decomp b) /. k) /. 2)))) by FUNCOP_1:13 .= (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3 .= dom (decomp (((decomp b) /. k) /. 2)) ; A17: dom (decomp (((decomp b) /. k) /. 2)) = Seg (len (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3; rng (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) c= 3 -tuples_on (Bags n) proof reconsider Gi = <*(((decomp b) /. k) /. 1)*> as Element of 1 -tuples_on (Bags n) by FINSEQ_2:98; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) or y in 3 -tuples_on (Bags n) ) assume y in rng (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) ; ::_thesis: y in 3 -tuples_on (Bags n) then consider i being set such that A18: i in dom (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) and A19: (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) . i = y by FUNCT_1:def_3; (decomp (((decomp b) /. k) /. 2)) . i in rng (decomp (((decomp b) /. k) /. 2)) by A16, A18, FUNCT_1:def_3; then reconsider Fi = (decomp (((decomp b) /. k) /. 2)) . i as Element of 2 -tuples_on (Bags n) ; reconsider i9 = i as Element of NAT by A18; ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) . i9 = <*(((decomp b) /. k) /. 1)*> by A16, A17, A18, FUNCOP_1:7; then y = Gi ^ Fi by A18, A19, PRE_POLY:def_4; hence y in 3 -tuples_on (Bags n) by FINSEQ_2:131; ::_thesis: verum end; then A20: ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) is FinSequence of 3 -tuples_on (Bags n) by FINSEQ_1:def_4; dbr . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) by A13, A14; hence y in (3 -tuples_on (Bags n)) * by A15, A20, FINSEQ_1:def_11; ::_thesis: verum end; then reconsider dbl = dbl, dbr = dbr as FinSequence of (3 -tuples_on (Bags n)) * by A3, FINSEQ_1:def_4; set fdbl = FlattenSeq dbl; set fdbr = FlattenSeq dbr; consider ls being FinSequence of the carrier of L such that A21: pqra . b = Sum ls and A22: len ls = len (decomp b) and A23: for k being Element of NAT st k in dom ls holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & ls /. k = ((p *' q) . b1) * (r . b2) ) by Def9; A24: dom dbr = dom (decomp b) by A12, FINSEQ_3:29; reconsider vfdbl = v * (FlattenSeq dbl), vfdbr = v * (FlattenSeq dbr) as FinSequence of the carrier of L by FINSEQ_2:32; consider vdbl being FinSequence of the carrier of L * such that A25: vdbl = ((dom dbl) --> v) ** dbl and A26: vfdbl = FlattenSeq vdbl by PRE_POLY:32; A27: dom v = 3 -tuples_on (Bags n) by FUNCT_2:def_1; now__::_thesis:_(_len_(Sum_vdbl)_=_len_ls_&_(_for_k_being_Nat_st_1_<=_k_&_k_<=_len_ls_holds_ (Sum_vdbl)_._k_=_ls_._k_)_) set f = Sum vdbl; A28: dom vdbl = (dom ((dom dbl) --> v)) /\ (dom dbl) by A25, PBOOLE:def_19 .= (dom dbl) /\ (dom dbl) by FUNCOP_1:13 .= dom dbl ; A29: dom (Sum vdbl) = dom vdbl by Th2; hence len (Sum vdbl) = len ls by A22, A1, A28, FINSEQ_3:29; ::_thesis: for k being Nat st 1 <= k & k <= len ls holds (Sum vdbl) . k = ls . k let k be Nat; ::_thesis: ( 1 <= k & k <= len ls implies (Sum vdbl) . k = ls . k ) assume A30: ( 1 <= k & k <= len ls ) ; ::_thesis: (Sum vdbl) . k = ls . k A31: k in dom (Sum vdbl) by A22, A1, A29, A28, A30, FINSEQ_3:25; then A32: (Sum vdbl) /. k = (Sum vdbl) . k by PARTFUN1:def_6; A33: dom ls = dom (Sum vdbl) by A22, A1, A29, A28, FINSEQ_3:29; then A34: ls /. k = ls . k by A31, PARTFUN1:def_6; consider b1, b2 being bag of n such that A35: (decomp b) /. k = <*b1,b2*> and A36: ls /. k = ((p *' q) . b1) * (r . b2) by A23, A33, A31; A37: len <*b1,b2*> = 2 by FINSEQ_1:44; then 1 in dom <*b1,b2*> by FINSEQ_3:25; then A38: ((decomp b) /. k) /. 1 = <*b1,b2*> . 1 by A35, PARTFUN1:def_6 .= b1 by FINSEQ_1:44 ; set dblk = dbl . k; set dbk2 = ((decomp b) /. k) /. 2; set ddbk1 = decomp (((decomp b) /. k) /. 1); A39: k in dom vdbl by A22, A1, A28, A30, FINSEQ_3:25; then A40: dbl . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) by A2, A28; then A41: dom (dbl . k) = (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) by PRE_POLY:def_4 .= (dom (decomp (((decomp b) /. k) /. 1))) /\ (Seg (len (decomp (((decomp b) /. k) /. 1)))) by FUNCOP_1:13 .= (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3 .= dom (decomp (((decomp b) /. k) /. 1)) ; set vdblk = v * (dbl . k); k in dom dbl by A22, A1, A30, FINSEQ_3:25; then dbl . k in rng dbl by FUNCT_1:def_3; then dbl . k is Element of (3 -tuples_on (Bags n)) * ; then reconsider dblk = dbl . k as FinSequence of 3 -tuples_on (Bags n) ; rng dblk c= 3 -tuples_on (Bags n) ; then A42: dom (v * (dbl . k)) = dom dblk by A27, RELAT_1:27; then A43: dom (v * (dbl . k)) = Seg (len (decomp (((decomp b) /. k) /. 1))) by A41, FINSEQ_1:def_3; reconsider b29 = b2 as Element of Bags n by PRE_POLY:def_12; consider pqs being FinSequence of the carrier of L such that A44: (p *' q) . b1 = Sum pqs and A45: len pqs = len (decomp b1) and A46: for i being Element of NAT st i in dom pqs holds ex b11, b12 being bag of n st ( (decomp b1) /. i = <*b11,b12*> & pqs /. i = (p . b11) * (q . b12) ) by Def9; A47: dom pqs = dom (pqs * (r . b2)) by Def2; 2 in dom <*b1,b2*> by A37, FINSEQ_3:25; then A48: ((decomp b) /. k) /. 2 = <*b1,b2*> . 2 by A35, PARTFUN1:def_6 .= b2 by FINSEQ_1:44 ; reconsider vdblk = v * (dbl . k) as FinSequence by A43, FINSEQ_1:def_2; A49: Sum (pqs * (r . b2)) = (Sum pqs) * (r . b2) by Th13; A50: dom (decomp (((decomp b) /. k) /. 1)) = Seg (len (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3; now__::_thesis:_(_len_vdblk_=_len_(pqs_*_(r_._b2))_&_(_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(pqs_*_(r_._b2))_holds_ (v_*_(dbl_._k))_._i_=_(pqs_*_(r_._b2))_._i_)_) A51: dom pqs = dom (pqs * (r . b2)) by Def2; thus len vdblk = len pqs by A45, A38, A41, A42, FINSEQ_3:29 .= len (pqs * (r . b2)) by A47, FINSEQ_3:29 ; ::_thesis: for i being Nat st 1 <= i & i <= len (pqs * (r . b2)) holds (v * (dbl . k)) . i = (pqs * (r . b2)) . i then A52: dom vdblk = dom (pqs * (r . b2)) by FINSEQ_3:29; let i be Nat; ::_thesis: ( 1 <= i & i <= len (pqs * (r . b2)) implies (v * (dbl . k)) . i = (pqs * (r . b2)) . i ) reconsider i9 = i as Element of NAT by ORDINAL1:def_12; assume A53: ( 1 <= i & i <= len (pqs * (r . b2)) ) ; ::_thesis: (v * (dbl . k)) . i = (pqs * (r . b2)) . i then A54: i in dom (pqs * (r . b2)) by FINSEQ_3:25; then consider b11, b12 being bag of n such that A55: (decomp b1) /. i = <*b11,b12*> and A56: pqs /. i = (p . b11) * (q . b12) by A46, A47; ( ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) . i9 = <*(((decomp b) /. k) /. 2)*> & (decomp b1) /. i = (decomp b1) . i ) by A38, A41, A50, A42, A52, A54, FUNCOP_1:7, PARTFUN1:def_6; then A57: dblk . i = <*b11,b12*> ^ <*b2*> by A48, A38, A40, A42, A52, A54, A55, PRE_POLY:def_4 .= <*b11,b12,b2*> by FINSEQ_1:43 ; reconsider b119 = b11, b129 = b12 as Element of Bags n by PRE_POLY:def_12; reconsider B = <*b119,b129,b29*> as Element of 3 -tuples_on (Bags n) by FINSEQ_2:104; A58: i in dom pqs by A47, A53, FINSEQ_3:25; thus (v * (dbl . k)) . i = v . (dblk . i) by A52, A54, FUNCT_1:12 .= ((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3)) by A11, A57 .= ((p . b119) * (q . (B /. 2))) * (r . (B /. 3)) by FINSEQ_4:18 .= ((p . b11) * (q . b12)) * (r . (B /. 3)) by FINSEQ_4:18 .= (pqs /. i) * (r . b2) by A56, FINSEQ_4:18 .= (pqs * (r . b2)) /. i by A58, Def2 .= (pqs * (r . b2)) . i by A58, A51, PARTFUN1:def_6 ; ::_thesis: verum end; then A59: vdblk = pqs * (r . b2) by FINSEQ_1:14; vdbl /. k = vdbl . k by A39, PARTFUN1:def_6 .= (((dom dbl) --> v) . k) * (dbl . k) by A25, A39, PBOOLE:def_19 .= pqs * (r . b2) by A28, A39, A59, FUNCOP_1:7 ; hence (Sum vdbl) . k = ls . k by A31, A36, A44, A49, A34, A32, MATRLIN:def_6; ::_thesis: verum end; then A60: Sum vdbl = ls by FINSEQ_1:14; consider vdbr being FinSequence of the carrier of L * such that A61: vdbr = ((dom dbr) --> v) ** dbr and A62: vfdbr = FlattenSeq vdbr by PRE_POLY:32; A63: Sum vfdbr = Sum (Sum vdbr) by A62, Th14; consider rs being FinSequence of the carrier of L such that A64: pqrb . b = Sum rs and A65: len rs = len (decomp b) and A66: for k being Element of NAT st k in dom rs holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & rs /. k = (p . b1) * ((q *' r) . b2) ) by Def9; now__::_thesis:_(_len_(Sum_vdbr)_=_len_rs_&_(_for_k_being_Nat_st_1_<=_k_&_k_<=_len_rs_holds_ (Sum_vdbr)_._k_=_rs_._k_)_) set f = Sum vdbr; A67: dom vdbr = (dom ((dom dbr) --> v)) /\ (dom dbr) by A61, PBOOLE:def_19 .= (dom dbr) /\ (dom dbr) by FUNCOP_1:13 .= dom dbr ; A68: dom (Sum vdbr) = dom vdbr by Th2; hence len (Sum vdbr) = len rs by A65, A12, A67, FINSEQ_3:29; ::_thesis: for k being Nat st 1 <= k & k <= len rs holds (Sum vdbr) . k = rs . k let k be Nat; ::_thesis: ( 1 <= k & k <= len rs implies (Sum vdbr) . k = rs . k ) assume A69: ( 1 <= k & k <= len rs ) ; ::_thesis: (Sum vdbr) . k = rs . k A70: k in dom (Sum vdbr) by A65, A12, A68, A67, A69, FINSEQ_3:25; then A71: (Sum vdbr) /. k = (Sum vdbr) . k by PARTFUN1:def_6; set dbrk = dbr . k; set dbk2 = ((decomp b) /. k) /. 1; set ddbk1 = decomp (((decomp b) /. k) /. 2); A72: k in dom vdbr by A65, A12, A67, A69, FINSEQ_3:25; then A73: dbr . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) by A13, A67; then A74: dom (dbr . k) = (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>)) by PRE_POLY:def_4 .= (dom (decomp (((decomp b) /. k) /. 2))) /\ (Seg (len (decomp (((decomp b) /. k) /. 2)))) by FUNCOP_1:13 .= (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3 .= dom (decomp (((decomp b) /. k) /. 2)) ; k in dom dbr by A65, A12, A69, FINSEQ_3:25; then dbr . k in rng dbr by FUNCT_1:def_3; then A75: dbr . k is Element of (3 -tuples_on (Bags n)) * ; set vdbrk = v * (dbr . k); A76: dom (decomp (((decomp b) /. k) /. 2)) = Seg (len (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3; reconsider dbrk = dbr . k as FinSequence of 3 -tuples_on (Bags n) by A75; rng dbrk c= 3 -tuples_on (Bags n) ; then A77: dom (v * (dbr . k)) = dom dbrk by A27, RELAT_1:27; then A78: dom (v * (dbr . k)) = Seg (len (decomp (((decomp b) /. k) /. 2))) by A74, FINSEQ_1:def_3; A79: dom rs = dom (Sum vdbr) by A65, A12, A68, A67, FINSEQ_3:29; then A80: rs /. k = rs . k by A70, PARTFUN1:def_6; consider b1, b2 being bag of n such that A81: (decomp b) /. k = <*b1,b2*> and A82: rs /. k = (p . b1) * ((q *' r) . b2) by A66, A79, A70; reconsider b19 = b1 as Element of Bags n by PRE_POLY:def_12; consider qrs being FinSequence of the carrier of L such that A83: (q *' r) . b2 = Sum qrs and A84: len qrs = len (decomp b2) and A85: for i being Element of NAT st i in dom qrs holds ex b11, b12 being bag of n st ( (decomp b2) /. i = <*b11,b12*> & qrs /. i = (q . b11) * (r . b12) ) by Def9; A86: dom qrs = dom ((p . b1) * qrs) by Def1; then A87: len qrs = len ((p . b1) * qrs) by FINSEQ_3:29; A88: len <*b1,b2*> = 2 by FINSEQ_1:44; then 1 in dom <*b1,b2*> by FINSEQ_3:25; then A89: ((decomp b) /. k) /. 1 = <*b1,b2*> . 1 by A81, PARTFUN1:def_6 .= b1 by FINSEQ_1:44 ; reconsider vdbrk = v * (dbr . k) as FinSequence by A78, FINSEQ_1:def_2; A90: Sum ((p . b1) * qrs) = (p . b1) * (Sum qrs) by Th12; 2 in dom <*b1,b2*> by A88, FINSEQ_3:25; then A91: ((decomp b) /. k) /. 2 = <*b1,b2*> . 2 by A81, PARTFUN1:def_6 .= b2 by FINSEQ_1:44 ; then A92: dom vdbrk = dom ((p . b1) * qrs) by A84, A74, A77, A86, FINSEQ_3:29; A93: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((p_._b1)_*_qrs)_holds_ (v_*_(dbr_._k))_._i_=_((p_._b1)_*_qrs)_._i let i be Nat; ::_thesis: ( 1 <= i & i <= len ((p . b1) * qrs) implies (v * (dbr . k)) . i = ((p . b1) * qrs) . i ) reconsider i9 = i as Element of NAT by ORDINAL1:def_12; assume A94: ( 1 <= i & i <= len ((p . b1) * qrs) ) ; ::_thesis: (v * (dbr . k)) . i = ((p . b1) * qrs) . i then A95: i in dom qrs by A86, FINSEQ_3:25; A96: i in dom dbrk by A84, A91, A74, A87, A94, FINSEQ_3:25; then consider b11, b12 being bag of n such that A97: (decomp b2) /. i = <*b11,b12*> and A98: qrs /. i = (q . b11) * (r . b12) by A85, A77, A86, A92; ( ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) . i9 = <*(((decomp b) /. k) /. 1)*> & (decomp b2) /. i = (decomp b2) . i ) by A91, A74, A76, A96, FUNCOP_1:7, PARTFUN1:def_6; then A99: dbrk . i = <*b1*> ^ <*b11,b12*> by A89, A91, A73, A96, A97, PRE_POLY:def_4 .= <*b1,b11,b12*> by FINSEQ_1:43 ; reconsider b119 = b11, b129 = b12 as Element of Bags n by PRE_POLY:def_12; reconsider B = <*b19,b119,b129*> as Element of 3 -tuples_on (Bags n) by FINSEQ_2:104; thus (v * (dbr . k)) . i = v . (dbrk . i) by A77, A96, FUNCT_1:12 .= ((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3)) by A11, A99 .= ((p . b1) * (q . (B /. 2))) * (r . (B /. 3)) by FINSEQ_4:18 .= ((p . b1) * (q . b11)) * (r . (B /. 3)) by FINSEQ_4:18 .= ((p . b1) * (q . b11)) * (r . b12) by FINSEQ_4:18 .= (p . b1) * (qrs /. i) by A98, GROUP_1:def_3 .= ((p . b1) * qrs) /. i by A95, Def1 .= ((p . b1) * qrs) . i by A86, A95, PARTFUN1:def_6 ; ::_thesis: verum end; len vdbrk = len ((p . b1) * qrs) by A84, A91, A74, A77, A87, FINSEQ_3:29; then A100: vdbrk = (p . b1) * qrs by A93, FINSEQ_1:14; vdbr /. k = vdbr . k by A72, PARTFUN1:def_6 .= (((dom dbr) --> v) . k) * (dbr . k) by A61, A72, PBOOLE:def_19 .= (p . b1) * qrs by A67, A72, A100, FUNCOP_1:7 ; hence (Sum vdbr) . k = rs . k by A70, A82, A83, A90, A80, A71, MATRLIN:def_6; ::_thesis: verum end; then A101: Sum vdbr = rs by FINSEQ_1:14; dom dbl = dom (decomp b) by A1, FINSEQ_3:29; then consider P being Permutation of (dom (FlattenSeq dbl)) such that A102: FlattenSeq dbr = (FlattenSeq dbl) * P by A2, A13, A24, PRE_POLY:74; rng (FlattenSeq dbl) c= 3 -tuples_on (Bags n) ; then dom vfdbl = dom (FlattenSeq dbl) by A27, RELAT_1:27; then reconsider P = P as Permutation of (dom vfdbl) ; A103: vfdbr = vfdbl * P by A102, RELAT_1:36; Sum vfdbl = Sum (Sum vdbl) by A26, Th14; hence pqra . b = pqrb . b by A21, A64, A60, A63, A101, A103, RLVECT_2:7; ::_thesis: verum end; hence (p *' q) *' r = p *' (q *' r) by FUNCT_2:63; ::_thesis: verum end; definition let n be Ordinal; let L be non empty right_complementable commutative Abelian add-associative right_zeroed doubleLoopStr ; let p, q be Series of n,L; :: original: *' redefine funcp *' q -> Series of n,L; commutativity for p, q being Series of n,L holds p *' q = q *' p proof let p, q be Series of n,L; ::_thesis: p *' q = q *' p reconsider pq = p *' q, qp = q *' p as Function of (Bags n), the carrier of L ; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_pq_._b_=_qp_._b let b be Element of Bags n; ::_thesis: pq . b = qp . b defpred S1[ set , set ] means ex b1, b2 being bag of n st ( (decomp b) . $1 = <*b1,b2*> & (decomp b) . $2 = <*b2,b1*> ); consider s being FinSequence of the carrier of L such that A1: pq . b = Sum s and A2: len s = len (decomp b) and A3: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by Def9; A4: dom s = dom (decomp b) by A2, FINSEQ_3:29; then reconsider ds = dom s as non empty set ; A5: now__::_thesis:_for_e_being_set_st_e_in_ds_holds_ ex_d_being_set_st_ (_d_in_ds_&_S1[e,d]_) let e be set ; ::_thesis: ( e in ds implies ex d being set st ( d in ds & S1[e,d] ) ) assume A6: e in ds ; ::_thesis: ex d being set st ( d in ds & S1[e,d] ) then consider b1, b2 being bag of n such that A7: (decomp b) /. e = <*b1,b2*> and A8: b = b1 + b2 by A4, PRE_POLY:68; consider d being Element of NAT such that A9: d in dom (decomp b) and A10: (decomp b) /. d = <*b2,b1*> by A8, PRE_POLY:69; reconsider d = d as set ; take d = d; ::_thesis: ( d in ds & S1[e,d] ) thus d in ds by A2, A9, FINSEQ_3:29; ::_thesis: S1[e,d] thus S1[e,d] ::_thesis: verum proof take b1 ; ::_thesis: ex b2 being bag of n st ( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> ) take b2 ; ::_thesis: ( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> ) thus ( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> ) by A4, A6, A7, A9, A10, PARTFUN1:def_6; ::_thesis: verum end; end; consider f being Function of ds,ds such that A11: for e being set st e in ds holds S1[e,f . e] from FUNCT_2:sch_1(A5); A12: dom f = ds by FUNCT_2:def_1; ds c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ds or x in rng f ) assume A13: x in ds ; ::_thesis: x in rng f then consider b1, b2 being bag of n such that A14: (decomp b) . x = <*b1,b2*> and A15: (decomp b) . (f . x) = <*b2,b1*> by A11; A16: f . x in rng f by A12, A13, FUNCT_1:def_3; then A17: f . (f . x) in rng f by A12, FUNCT_1:def_3; consider b3, b4 being bag of n such that A18: (decomp b) . (f . x) = <*b3,b4*> and A19: (decomp b) . (f . (f . x)) = <*b4,b3*> by A11, A16; ( b3 = b2 & b4 = b1 ) by A15, A18, FINSEQ_1:77; hence x in rng f by A4, A13, A17, A14, A19, FUNCT_1:def_4; ::_thesis: verum end; then A20: rng f = ds by XBOOLE_0:def_10; f is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A21: x1 in dom f and A22: x2 in dom f and A23: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider b3, b4 being bag of n such that A24: (decomp b) . x2 = <*b3,b4*> and A25: (decomp b) . (f . x2) = <*b4,b3*> by A11, A22; consider b1, b2 being bag of n such that A26: (decomp b) . x1 = <*b1,b2*> and A27: (decomp b) . (f . x1) = <*b2,b1*> by A11, A21; ( b2 = b4 & b1 = b3 ) by A23, A27, A25, FINSEQ_1:77; hence x1 = x2 by A4, A21, A22, A26, A24, FUNCT_1:def_4; ::_thesis: verum end; then reconsider f = f as Permutation of (dom s) by A20, FUNCT_2:57; consider t being FinSequence of the carrier of L such that A28: qp . b = Sum t and A29: len t = len (decomp b) and A30: for k being Element of NAT st k in dom t holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & t /. k = (q . b1) * (p . b2) ) by Def9; A31: dom t = dom (decomp b) by A29, FINSEQ_3:29; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_t_holds_ t_._i_=_s_._(f_._i) let i be Element of NAT ; ::_thesis: ( i in dom t implies t . i = s . (f . i) ) reconsider fi = f . i as Element of NAT ; A32: dom s = dom (decomp b) by A2, FINSEQ_3:29; assume A33: i in dom t ; ::_thesis: t . i = s . (f . i) then consider b1, b2 being bag of n such that A34: (decomp b) /. i = <*b1,b2*> and A35: t /. i = (q . b1) * (p . b2) by A30; A36: t /. i = t . i by A33, PARTFUN1:def_6; consider b5, b6 being bag of n such that A37: (decomp b) . i = <*b5,b6*> and A38: (decomp b) . (f . i) = <*b6,b5*> by A4, A31, A11, A33; dom s = dom t by A2, A29, FINSEQ_3:29; then (decomp b) /. i = (decomp b) . i by A33, A32, PARTFUN1:def_6; then A39: ( b1 = b5 & b2 = b6 ) by A34, A37, FINSEQ_1:77; A40: f . i in rng f by A4, A31, A12, A33, FUNCT_1:def_3; then A41: s /. fi = s . fi by PARTFUN1:def_6; consider b3, b4 being bag of n such that A42: (decomp b) /. fi = <*b3,b4*> and A43: s /. fi = (p . b3) * (q . b4) by A3, A40; A44: (decomp b) /. fi = (decomp b) . fi by A40, A32, PARTFUN1:def_6; then b3 = b6 by A42, A38, FINSEQ_1:77; hence t . i = s . (f . i) by A35, A42, A43, A38, A36, A41, A44, A39, FINSEQ_1:77; ::_thesis: verum end; hence pq . b = qp . b by A1, A2, A28, A29, RLVECT_2:6; ::_thesis: verum end; hence p *' q = q *' p by FUNCT_2:63; ::_thesis: verum end; end; theorem :: POLYNOM1:28 for n being Ordinal for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L) proof let n be Ordinal; ::_thesis: for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L) let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L) let p be Series of n,L; ::_thesis: p *' (0_ (n,L)) = 0_ (n,L) set Z = 0_ (n,L); now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_*'_(0__(n,L)))_._b_=_(0__(n,L))_._b let b be Element of Bags n; ::_thesis: (p *' (0_ (n,L))) . b = (0_ (n,L)) . b consider s being FinSequence of the carrier of L such that A1: (p *' (0_ (n,L))) . b = Sum s and len s = len (decomp b) and A2: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((0_ (n,L)) . b2) ) by Def9; now__::_thesis:_for_k_being_Nat_st_k_in_dom_s_holds_ s_/._k_=_0._L let k be Nat; ::_thesis: ( k in dom s implies s /. k = 0. L ) assume k in dom s ; ::_thesis: s /. k = 0. L then consider b1, b2 being bag of n such that (decomp b) /. k = <*b1,b2*> and A3: s /. k = (p . b1) * ((0_ (n,L)) . b2) by A2; thus s /. k = (p . b1) * (0. L) by A3, Th22 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; then Sum s = 0. L by MATRLIN:11; hence (p *' (0_ (n,L))) . b = (0_ (n,L)) . b by A1, Th22; ::_thesis: verum end; hence p *' (0_ (n,L)) = 0_ (n,L) by FUNCT_2:63; ::_thesis: verum end; theorem Th29: :: POLYNOM1:29 for n being Ordinal for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds p *' (1_ (n,L)) = p proof let n be Ordinal; ::_thesis: for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds p *' (1_ (n,L)) = p let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds p *' (1_ (n,L)) = p let p be Series of n,L; ::_thesis: p *' (1_ (n,L)) = p set O = 1_ (n,L); set cL = the carrier of L; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_*'_(1__(n,L)))_._b_=_p_._b let b be Element of Bags n; ::_thesis: (p *' (1_ (n,L))) . b = p . b consider s being FinSequence of the carrier of L such that A1: (p *' (1_ (n,L))) . b = Sum s and A2: len s = len (decomp b) and A3: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((1_ (n,L)) . b2) ) by Def9; consider t being FinSequence of the carrier of L, s1 being Element of the carrier of L such that A4: s = t ^ <*s1*> by A2, FINSEQ_2:19; A5: now__::_thesis:_Sum_t_=_0._L percases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ; suppose t = <*> the carrier of L ; ::_thesis: Sum t = 0. L hence Sum t = 0. L by RLVECT_1:43; ::_thesis: verum end; supposeA6: t <> <*> the carrier of L ; ::_thesis: Sum t = 0. L now__::_thesis:_for_k_being_Nat_st_k_in_dom_t_holds_ t_/._k_=_0._L let k be Nat; ::_thesis: ( k in dom t implies t /. b1 = 0. L ) A7: len s = (len t) + (len <*s1*>) by A4, FINSEQ_1:22 .= (len t) + 1 by FINSEQ_1:39 ; assume A8: k in dom t ; ::_thesis: t /. b1 = 0. L then A9: t /. k = t . k by PARTFUN1:def_6 .= s . k by A4, A8, FINSEQ_1:def_7 ; k <= len t by A8, FINSEQ_3:25; then A10: k < len s by A7, NAT_1:13; A11: 1 <= k by A8, FINSEQ_3:25; then A12: k in dom (decomp b) by A2, A10, FINSEQ_3:25; A13: dom s = dom (decomp b) by A2, FINSEQ_3:29; then A14: s /. k = s . k by A12, PARTFUN1:def_6; percases ( 1 < k or k = 1 ) by A11, XXREAL_0:1; supposeA15: 1 < k ; ::_thesis: t /. b1 = 0. L consider b1, b2 being bag of n such that A16: (decomp b) /. k = <*b1,b2*> and A17: s /. k = (p . b1) * ((1_ (n,L)) . b2) by A3, A13, A12; b2 <> EmptyBag n by A2, A10, A15, A16, PRE_POLY:72; hence t /. k = (p . b1) * (0. L) by A9, A14, A17, Th25 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; supposeA18: k = 1 ; ::_thesis: t /. b1 = 0. L A19: now__::_thesis:_not_b_=_EmptyBag_n assume b = EmptyBag n ; ::_thesis: contradiction then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73; then (len t) + 1 = 0 + 1 by A2, A7, FINSEQ_1:39; hence contradiction by A6; ::_thesis: verum end; consider b1, b2 being bag of n such that A20: (decomp b) /. k = <*b1,b2*> and A21: s /. k = (p . b1) * ((1_ (n,L)) . b2) by A3, A13, A12; (decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71; then ( b1 = EmptyBag n & b2 = b ) by A18, A20, FINSEQ_1:77; then s . k = (p . (EmptyBag n)) * (0. L) by A14, A21, A19, Th25 .= 0. L by VECTSP_1:6 ; hence t /. k = 0. L by A9; ::_thesis: verum end; end; end; hence Sum t = 0. L by MATRLIN:11; ::_thesis: verum end; end; end; A22: s . (len s) = (t ^ <*s1*>) . ((len t) + 1) by A4, FINSEQ_2:16 .= s1 by FINSEQ_1:42 ; A23: Sum s = (Sum t) + (Sum <*s1*>) by A4, RLVECT_1:41; not s is empty by A2; then A24: len s in dom s by FINSEQ_5:6; then consider b1, b2 being bag of n such that A25: (decomp b) /. (len s) = <*b1,b2*> and A26: s /. (len s) = (p . b1) * ((1_ (n,L)) . b2) by A3; A27: s /. (len s) = s . (len s) by A24, PARTFUN1:def_6; (decomp b) /. (len s) = <*b,(EmptyBag n)*> by A2, PRE_POLY:71; then A28: ( b1 = b & b2 = EmptyBag n ) by A25, FINSEQ_1:77; Sum <*s1*> = s1 by RLVECT_1:44 .= (p . b) * (1. L) by A26, A28, A22, A27, Th25 .= p . b by VECTSP_1:def_4 ; hence (p *' (1_ (n,L))) . b = p . b by A1, A23, A5, RLVECT_1:4; ::_thesis: verum end; hence p *' (1_ (n,L)) = p by FUNCT_2:63; ::_thesis: verum end; theorem Th30: :: POLYNOM1:30 for n being Ordinal for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds (1_ (n,L)) *' p = p proof let n be Ordinal; ::_thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for p being Series of n,L holds (1_ (n,L)) *' p = p let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds (1_ (n,L)) *' p = p let p be Series of n,L; ::_thesis: (1_ (n,L)) *' p = p set O = 1_ (n,L); set cL = the carrier of L; now__::_thesis:_for_b_being_Element_of_Bags_n_holds_((1__(n,L))_*'_p)_._b_=_p_._b let b be Element of Bags n; ::_thesis: ((1_ (n,L)) *' p) . b = p . b consider s being FinSequence of the carrier of L such that A1: ((1_ (n,L)) *' p) . b = Sum s and A2: len s = len (decomp b) and A3: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = ((1_ (n,L)) . b1) * (p . b2) ) by Def9; not s is empty by A2; then consider s1 being Element of the carrier of L, t being FinSequence of the carrier of L such that A4: s1 = s . 1 and A5: s = <*s1*> ^ t by FINSEQ_3:102; A6: Sum s = (Sum <*s1*>) + (Sum t) by A5, RLVECT_1:41; A7: now__::_thesis:_Sum_t_=_0._L percases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ; suppose t = <*> the carrier of L ; ::_thesis: Sum t = 0. L hence Sum t = 0. L by RLVECT_1:43; ::_thesis: verum end; supposeA8: t <> <*> the carrier of L ; ::_thesis: Sum t = 0. L now__::_thesis:_for_k_being_Nat_st_k_in_dom_t_holds_ t_/._k_=_0._L let k be Nat; ::_thesis: ( k in dom t implies t /. b1 = 0. L ) A9: len s = (len t) + (len <*s1*>) by A5, FINSEQ_1:22 .= (len t) + 1 by FINSEQ_1:39 ; assume A10: k in dom t ; ::_thesis: t /. b1 = 0. L then A11: t /. k = t . k by PARTFUN1:def_6 .= s . (k + 1) by A5, A10, FINSEQ_3:103 ; 1 <= k by A10, FINSEQ_3:25; then A12: 1 < k + 1 by NAT_1:13; k <= len t by A10, FINSEQ_3:25; then A13: k + 1 <= len s by A9, XREAL_1:6; then A14: k + 1 in dom (decomp b) by A2, A12, FINSEQ_3:25; A15: dom s = dom (decomp b) by A2, FINSEQ_3:29; then A16: s /. (k + 1) = s . (k + 1) by A14, PARTFUN1:def_6; percases ( k + 1 < len s or k + 1 = len s ) by A13, XXREAL_0:1; supposeA17: k + 1 < len s ; ::_thesis: t /. b1 = 0. L consider b1, b2 being bag of n such that A18: (decomp b) /. (k + 1) = <*b1,b2*> and A19: s /. (k + 1) = ((1_ (n,L)) . b1) * (p . b2) by A3, A15, A14; b1 <> EmptyBag n by A2, A12, A17, A18, PRE_POLY:72; hence t /. k = (0. L) * (p . b2) by A11, A16, A19, Th25 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; supposeA20: k + 1 = len s ; ::_thesis: t /. b1 = 0. L A21: now__::_thesis:_not_b_=_EmptyBag_n assume b = EmptyBag n ; ::_thesis: contradiction then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73; then (len t) + 1 = 0 + 1 by A2, A9, FINSEQ_1:39; hence contradiction by A8; ::_thesis: verum end; consider b1, b2 being bag of n such that A22: (decomp b) /. (k + 1) = <*b1,b2*> and A23: s /. (k + 1) = ((1_ (n,L)) . b1) * (p . b2) by A3, A15, A14; (decomp b) /. (len s) = <*b,(EmptyBag n)*> by A2, PRE_POLY:71; then ( b2 = EmptyBag n & b1 = b ) by A20, A22, FINSEQ_1:77; then s . (k + 1) = (0. L) * (p . (EmptyBag n)) by A16, A23, A21, Th25 .= 0. L by VECTSP_1:7 ; hence t /. k = 0. L by A11; ::_thesis: verum end; end; end; hence Sum t = 0. L by MATRLIN:11; ::_thesis: verum end; end; end; A24: not s is empty by A2; then consider b1, b2 being bag of n such that A25: (decomp b) /. 1 = <*b1,b2*> and A26: s /. 1 = ((1_ (n,L)) . b1) * (p . b2) by A3, FINSEQ_5:6; 1 in dom s by A24, FINSEQ_5:6; then A27: s /. 1 = s . 1 by PARTFUN1:def_6; (decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71; then A28: ( b2 = b & b1 = EmptyBag n ) by A25, FINSEQ_1:77; Sum <*s1*> = s1 by RLVECT_1:44 .= (1. L) * (p . b) by A4, A26, A28, A27, Th25 .= p . b by VECTSP_1:def_6 ; hence ((1_ (n,L)) *' p) . b = p . b by A1, A6, A7, RLVECT_1:4; ::_thesis: verum end; hence (1_ (n,L)) *' p = p by FUNCT_2:63; ::_thesis: verum end; begin registration let n be set ; let S be non empty ZeroStr ; cluster Relation-like Bags n -defined the carrier of S -valued Function-like non empty total quasi_total finite-Support for Element of bool [:(Bags n), the carrier of S:]; existence ex b1 being Series of n,S st b1 is finite-Support proof reconsider P = (Bags n) --> (0. S) as Function of (Bags n), the carrier of S ; reconsider P = P as Function of (Bags n),S ; reconsider P = P as Series of n,S ; take P ; ::_thesis: P is finite-Support for x being Element of Bags n holds ( x in {} iff P . x <> 0. S ) by FUNCOP_1:7; then Support P = {} (Bags n) by Def3; hence Support P is finite ; :: according to POLYNOM1:def_4 ::_thesis: verum end; end; definition let n be Ordinal; let S be non empty ZeroStr ; mode Polynomial of n,S is finite-Support Series of n,S; end; registration let n be Ordinal; let L be non empty right_zeroed addLoopStr ; let p, q be Polynomial of n,L; clusterp + q -> finite-Support ; coherence p + q is finite-Support proof set Sp = Support p; set Sq = Support q; ( Support p is finite & Support q is finite ) by Def4; then (Support p) \/ (Support q) is finite ; then Support (p + q) is finite by Th20, FINSET_1:1; hence p + q is finite-Support by Def4; ::_thesis: verum end; end; registration let n be Ordinal; let L be non empty right_complementable add-associative right_zeroed addLoopStr ; let p be Polynomial of n,L; cluster - p -> finite-Support ; coherence - p is finite-Support proof set f = - p; A1: Support (- p) c= Support p proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support (- p) or x in Support p ) assume A2: x in Support (- p) ; ::_thesis: x in Support p then reconsider x9 = x as Element of Bags n ; (- p) . x9 <> 0. L by A2, Def3; then - (p . x9) <> 0. L by Th17; then p . x9 <> 0. L by RLVECT_1:12; hence x in Support p by Def3; ::_thesis: verum end; Support p is finite by Def4; hence - p is finite-Support by A1, Def4; ::_thesis: verum end; end; registration let n be Element of NAT ; let L be non empty right_complementable add-associative right_zeroed addLoopStr ; let p, q be Polynomial of n,L; clusterp - q -> finite-Support ; coherence p - q is finite-Support ; end; registration let n be Ordinal; let S be non empty ZeroStr ; cluster 0_ (n,S) -> finite-Support ; coherence 0_ (n,S) is finite-Support proof set Z = 0_ (n,S); now__::_thesis:_for_x_being_set_holds_not_x_in_Support_(0__(n,S)) given x being set such that A1: x in Support (0_ (n,S)) ; ::_thesis: contradiction reconsider x = x as Element of Bags n by A1; (0_ (n,S)) . x = 0. S by FUNCOP_1:7; hence contradiction by A1, Def3; ::_thesis: verum end; then Support (0_ (n,S)) = {} by XBOOLE_0:def_1; hence 0_ (n,S) is finite-Support by Def4; ::_thesis: verum end; end; registration let n be Ordinal; let L be non trivial right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ; cluster 1_ (n,L) -> finite-Support ; coherence 1_ (n,L) is finite-Support proof reconsider O = (0_ (n,L)) +* ((EmptyBag n),(1. L)) as Function of (Bags n), the carrier of L ; reconsider O9 = O as Function of (Bags n),L ; reconsider O9 = O9 as Series of n,L ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Support_O9_implies_not_x_<>_EmptyBag_n_)_&_(_x_=_EmptyBag_n_implies_x_in_Support_O9_)_) let x be set ; ::_thesis: ( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) ) hereby ::_thesis: ( x = EmptyBag n implies x in Support O9 ) assume A1: x in Support O9 ; ::_thesis: not x <> EmptyBag n then reconsider x9 = x as Element of Bags n ; assume x <> EmptyBag n ; ::_thesis: contradiction then O9 . x = (0_ (n,L)) . x9 by FUNCT_7:32 .= 0. L by FUNCOP_1:7 ; hence contradiction by A1, Def3; ::_thesis: verum end; assume A2: x = EmptyBag n ; ::_thesis: x in Support O9 dom (0_ (n,L)) = Bags n by FUNCOP_1:13; then O9 . x <> 0. L by A2, FUNCT_7:31; hence x in Support O9 by A2, Def3; ::_thesis: verum end; then Support O9 = {(EmptyBag n)} by TARSKI:def_1; hence 1_ (n,L) is finite-Support by Def4; ::_thesis: verum end; end; registration let n be Ordinal; let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; let p, q be Polynomial of n,L; clusterp *' q -> finite-Support ; coherence p *' q is finite-Support proof deffunc H1( Element of Bags n, Element of Bags n) -> set = n + L; set D = { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } ; A1: Support q is finite by Def4; A2: Support (p *' q) c= { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } proof let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in Support (p *' q) or x9 in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } ) assume A3: x9 in Support (p *' q) ; ::_thesis: x9 in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } then reconsider b = x9 as Element of Bags n ; consider s being FinSequence of the carrier of L such that A4: (p *' q) . b = Sum s and A5: len s = len (decomp b) and A6: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of n st ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by Def9; (p *' q) . b <> 0. L by A3, Def3; then consider k being Nat such that A7: k in dom s and A8: s /. k <> 0. L by A4, MATRLIN:11; consider b1, b2 being bag of n such that A9: (decomp b) /. k = <*b1,b2*> and A10: s /. k = (p . b1) * (q . b2) by A6, A7; A11: b1 in Bags n by PRE_POLY:def_12; A12: b2 in Bags n by PRE_POLY:def_12; q . b2 <> 0. L by A8, A10, VECTSP_1:6; then A13: b2 in Support q by A12, Def3; p . b1 <> 0. L by A8, A10, VECTSP_1:7; then A14: b1 in Support p by A11, Def3; k in dom (decomp b) by A5, A7, FINSEQ_3:29; then consider b19, b29 being bag of n such that A15: (decomp b) /. k = <*b19,b29*> and A16: b = b19 + b29 by PRE_POLY:68; ( b19 = b1 & b29 = b2 ) by A9, A15, FINSEQ_1:77; hence x9 in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } by A14, A13, A16; ::_thesis: verum end; A17: Support p is finite by Def4; { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } is finite from FRAENKEL:sch_22(A17, A1); hence p *' q is finite-Support by A2, Def4; ::_thesis: verum end; end; begin definition let n be Ordinal; let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; func Polynom-Ring (n,L) -> non empty strict doubleLoopStr means :Def10: :: POLYNOM1:def 10 ( ( for x being set holds ( x in the carrier of it iff x is Polynomial of n,L ) ) & ( for x, y being Element of it for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of it for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. it = 0_ (n,L) & 1. it = 1_ (n,L) ); existence ex b1 being non empty strict doubleLoopStr st ( ( for x being set holds ( x in the carrier of b1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b1 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b1 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. b1 = 0_ (n,L) & 1. b1 = 1_ (n,L) ) proof reconsider Z = (Bags n) --> (0. L) as Function of (Bags n), the carrier of L ; defpred S1[ set , set , set ] means ex p, q, r being Polynomial of n,L st ( p = $1 & q = $2 & r = $3 & p *' q = r ); defpred S2[ set , set , set ] means ex p, q, r being Polynomial of n,L st ( p = $1 & q = $2 & r = $3 & p + q = r ); set x9 = the finite-Support Series of n,L; defpred S3[ set ] means ex x9 being Series of n,L st ( x9 = $1 & x9 is finite-Support ); consider P being Subset of (Funcs ((Bags n), the carrier of L)) such that A1: for x being Element of Funcs ((Bags n), the carrier of L) holds ( x in P iff S3[x] ) from SUBSET_1:sch_3(); the finite-Support Series of n,L in Funcs ((Bags n), the carrier of L) by FUNCT_2:8; then reconsider P = P as non empty Subset of (Funcs ((Bags n), the carrier of L)) by A1; A2: now__::_thesis:_for_x,_y_being_Element_of_P_ex_u_being_Element_of_P_st_S2[x,y,u] let x, y be Element of P; ::_thesis: ex u being Element of P st S2[x,y,u] reconsider p = x, q = y as Element of Funcs ((Bags n), the carrier of L) ; consider p9 being Series of n,L such that A3: p9 = p and A4: p9 is finite-Support by A1; consider q9 being Series of n,L such that A5: q9 = q and A6: q9 is finite-Support by A1; reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A4, A6; set r = p9 + q9; p9 + q9 in Funcs ((Bags n), the carrier of L) by FUNCT_2:8; then reconsider u = p9 + q9 as Element of P by A1; take u = u; ::_thesis: S2[x,y,u] thus S2[x,y,u] by A3, A5; ::_thesis: verum end; consider fadd being Function of [:P,P:],P such that A7: for x, y being Element of P holds S2[x,y,fadd . (x,y)] from BINOP_1:sch_3(A2); A8: now__::_thesis:_for_x,_y_being_Element_of_P_ex_u_being_Element_of_P_st_S1[x,y,u] let x, y be Element of P; ::_thesis: ex u being Element of P st S1[x,y,u] reconsider p = x, q = y as Element of Funcs ((Bags n), the carrier of L) ; consider p9 being Series of n,L such that A9: p9 = p and A10: p9 is finite-Support by A1; consider q9 being Series of n,L such that A11: q9 = q and A12: q9 is finite-Support by A1; reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A10, A12; set r = p9 *' q9; p9 *' q9 in Funcs ((Bags n), the carrier of L) by FUNCT_2:8; then reconsider u = p9 *' q9 as Element of P by A1; take u = u; ::_thesis: S1[x,y,u] thus S1[x,y,u] by A9, A11; ::_thesis: verum end; consider fmult being Function of [:P,P:],P such that A13: for x, y being Element of P holds S1[x,y,fmult . (x,y)] from BINOP_1:sch_3(A8); reconsider ZZ = Z as Element of Funcs ((Bags n), the carrier of L) by FUNCT_2:8; reconsider Z9 = Z as Function of (Bags n),L ; reconsider Z9 = Z9 as Series of n,L ; now__::_thesis:_for_x_being_set_holds_not_x_in_Support_Z9 given x being set such that A14: x in Support Z9 ; ::_thesis: contradiction reconsider x = x as Element of Bags n by A14; Z9 . x = 0. L by FUNCOP_1:7; hence contradiction by A14, Def3; ::_thesis: verum end; then Support Z9 = {} by XBOOLE_0:def_1; then Z9 is finite-Support by Def4; then ZZ in P by A1; then reconsider Ze = Z as Element of P ; reconsider O = Z +* ((EmptyBag n),(1. L)) as Function of (Bags n), the carrier of L ; reconsider O9 = O as Function of (Bags n),L ; reconsider O9 = O9 as Series of n,L ; reconsider O = O as Element of Funcs ((Bags n), the carrier of L) by FUNCT_2:8; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Support_O9_implies_not_x_<>_EmptyBag_n_)_&_(_x_=_EmptyBag_n_implies_x_in_Support_O9_)_) let x be set ; ::_thesis: ( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) ) hereby ::_thesis: ( x = EmptyBag n implies x in Support O9 ) assume A15: x in Support O9 ; ::_thesis: not x <> EmptyBag n then reconsider x9 = x as Element of Bags n ; assume x <> EmptyBag n ; ::_thesis: contradiction then O9 . x = Z . x9 by FUNCT_7:32 .= 0. L by FUNCOP_1:7 ; hence contradiction by A15, Def3; ::_thesis: verum end; assume A16: x = EmptyBag n ; ::_thesis: x in Support O9 dom Z = Bags n by FUNCOP_1:13; then O9 . x <> 0. L by A16, FUNCT_7:31; hence x in Support O9 by A16, Def3; ::_thesis: verum end; then Support O9 = {(EmptyBag n)} by TARSKI:def_1; then O9 is finite-Support by Def4; then reconsider O = O as Element of P by A1; reconsider R = doubleLoopStr(# P,fadd,fmult,O,Ze #) as non empty strict doubleLoopStr ; take R ; ::_thesis: ( ( for x being set holds ( x in the carrier of R iff x is Polynomial of n,L ) ) & ( for x, y being Element of R for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of R for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. R = 0_ (n,L) & 1. R = 1_ (n,L) ) thus for x being set holds ( x in the carrier of R iff x is Polynomial of n,L ) ::_thesis: ( ( for x, y being Element of R for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of R for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. R = 0_ (n,L) & 1. R = 1_ (n,L) ) proof let x be set ; ::_thesis: ( x in the carrier of R iff x is Polynomial of n,L ) hereby ::_thesis: ( x is Polynomial of n,L implies x in the carrier of R ) assume A17: x in the carrier of R ; ::_thesis: x is Polynomial of n,L then reconsider xx = x as Element of Funcs ((Bags n), the carrier of L) ; ex x9 being Series of n,L st ( x9 = xx & x9 is finite-Support ) by A1, A17; hence x is Polynomial of n,L ; ::_thesis: verum end; assume A18: x is Polynomial of n,L ; ::_thesis: x in the carrier of R then x is Element of Funcs ((Bags n), the carrier of L) by FUNCT_2:8; hence x in the carrier of R by A1, A18; ::_thesis: verum end; hereby ::_thesis: ( ( for x, y being Element of R for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. R = 0_ (n,L) & 1. R = 1_ (n,L) ) let x, y be Element of R; ::_thesis: for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q let p, q be Polynomial of n,L; ::_thesis: ( x = p & y = q implies x + y = p + q ) assume A19: ( x = p & y = q ) ; ::_thesis: x + y = p + q ex p9, q9, r9 being Polynomial of n,L st ( p9 = x & q9 = y & r9 = fadd . (x,y) & p9 + q9 = r9 ) by A7; hence x + y = p + q by A19; ::_thesis: verum end; hereby ::_thesis: ( 0. R = 0_ (n,L) & 1. R = 1_ (n,L) ) let x, y be Element of R; ::_thesis: for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q let p, q be Polynomial of n,L; ::_thesis: ( x = p & y = q implies x * y = p *' q ) assume A20: ( x = p & y = q ) ; ::_thesis: x * y = p *' q ex p9, q9, r9 being Polynomial of n,L st ( p9 = x & q9 = y & r9 = fmult . (x,y) & p9 *' q9 = r9 ) by A13; hence x * y = p *' q by A20; ::_thesis: verum end; thus 0. R = 0_ (n,L) ; ::_thesis: 1. R = 1_ (n,L) thus 1. R = 1_ (n,L) ; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds ( x in the carrier of b1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b1 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b1 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. b1 = 0_ (n,L) & 1. b1 = 1_ (n,L) & ( for x being set holds ( x in the carrier of b2 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b2 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b2 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. b2 = 0_ (n,L) & 1. b2 = 1_ (n,L) holds b1 = b2 proof let it1, it2 be non empty strict doubleLoopStr ; ::_thesis: ( ( for x being set holds ( x in the carrier of it1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of it1 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of it1 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. it1 = 0_ (n,L) & 1. it1 = 1_ (n,L) & ( for x being set holds ( x in the carrier of it2 iff x is Polynomial of n,L ) ) & ( for x, y being Element of it2 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of it2 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. it2 = 0_ (n,L) & 1. it2 = 1_ (n,L) implies it1 = it2 ) assume that A21: for x being set holds ( x in the carrier of it1 iff x is Polynomial of n,L ) and A22: for x, y being Element of it1 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q and A23: for x, y being Element of it1 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q and A24: ( 0. it1 = 0_ (n,L) & 1. it1 = 1_ (n,L) ) and A25: for x being set holds ( x in the carrier of it2 iff x is Polynomial of n,L ) and A26: for x, y being Element of it2 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q and A27: for x, y being Element of it2 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q and A28: ( 0. it2 = 0_ (n,L) & 1. it2 = 1_ (n,L) ) ; ::_thesis: it1 = it2 A29: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_carrier_of_it1_implies_x_in_the_carrier_of_it2_)_&_(_x_in_the_carrier_of_it2_implies_x_in_the_carrier_of_it1_)_) let x be set ; ::_thesis: ( ( x in the carrier of it1 implies x in the carrier of it2 ) & ( x in the carrier of it2 implies x in the carrier of it1 ) ) hereby ::_thesis: ( x in the carrier of it2 implies x in the carrier of it1 ) assume x in the carrier of it1 ; ::_thesis: x in the carrier of it2 then x is Polynomial of n,L by A21; hence x in the carrier of it2 by A25; ::_thesis: verum end; assume x in the carrier of it2 ; ::_thesis: x in the carrier of it1 then x is Polynomial of n,L by A25; hence x in the carrier of it1 by A21; ::_thesis: verum end; then A30: the carrier of it1 = the carrier of it2 by TARSKI:1; A31: now__::_thesis:_for_a,_b_being_Element_of_it1_holds_the_multF_of_it1_._(a,b)_=_the_multF_of_it2_._(a,b) let a, b be Element of it1; ::_thesis: the multF of it1 . (a,b) = the multF of it2 . (a,b) reconsider a9 = a, b9 = b as Element of it2 by A29; reconsider a19 = a9, b19 = b9 as Element of it2 ; reconsider p = a, q = b as Polynomial of n,L by A21; reconsider a1 = a, b1 = b as Element of it1 ; thus the multF of it1 . (a,b) = a1 * b1 .= p *' q by A23 .= a19 * b19 by A27 .= the multF of it2 . (a,b) ; ::_thesis: verum end; now__::_thesis:_for_a,_b_being_Element_of_it1_holds_the_addF_of_it1_._(a,b)_=_the_addF_of_it2_._(a,b) let a, b be Element of it1; ::_thesis: the addF of it1 . (a,b) = the addF of it2 . (a,b) reconsider a9 = a, b9 = b as Element of it2 by A29; reconsider a19 = a9, b19 = b9 as Element of it2 ; reconsider p = a, q = b as Polynomial of n,L by A21; reconsider a1 = a, b1 = b as Element of it1 ; thus the addF of it1 . (a,b) = a1 + b1 .= p + q by A22 .= a19 + b19 by A26 .= the addF of it2 . (a,b) ; ::_thesis: verum end; then the addF of it1 = the addF of it2 by A30, BINOP_1:2; hence it1 = it2 by A24, A28, A30, A31, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def10 defines Polynom-Ring POLYNOM1:def_10_:_ for n being Ordinal for L being non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr for b3 being non empty strict doubleLoopStr holds ( b3 = Polynom-Ring (n,L) iff ( ( for x being set holds ( x in the carrier of b3 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b3 for p, q being Polynomial of n,L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b3 for p, q being Polynomial of n,L st x = p & y = q holds x * y = p *' q ) & 0. b3 = 0_ (n,L) & 1. b3 = 1_ (n,L) ) ); registration let n be Ordinal; let L be non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring (n,L) -> non empty strict Abelian ; coherence Polynom-Ring (n,L) is Abelian proof set Pm = Polynom-Ring (n,L); let v, w be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v reconsider p = v, q = w as Polynomial of n,L by Def10; thus v + w = q + p by Def10 .= w + v by Def10 ; ::_thesis: verum end; end; registration let n be Ordinal; let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring (n,L) -> non empty strict add-associative ; coherence Polynom-Ring (n,L) is add-associative proof set Pm = Polynom-Ring (n,L); let u, v, w be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w) reconsider o = u, p = v, q = w as Polynomial of n,L by Def10; A1: v + w = p + q by Def10; u + v = o + p by Def10; hence (u + v) + w = (o + p) + q by Def10 .= o + (p + q) by Th21 .= u + (v + w) by A1, Def10 ; ::_thesis: verum end; end; registration let n be Ordinal; let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring (n,L) -> non empty strict right_zeroed ; coherence Polynom-Ring (n,L) is right_zeroed proof let v be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (Polynom-Ring (n,L))) = v reconsider p = v as Polynomial of n,L by Def10; 0. (Polynom-Ring (n,L)) = 0_ (n,L) by Def10; hence v + (0. (Polynom-Ring (n,L))) = p + (0_ (n,L)) by Def10 .= v by Th23 ; ::_thesis: verum end; end; registration let n be Ordinal; let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring (n,L) -> non empty right_complementable strict ; coherence Polynom-Ring (n,L) is right_complementable proof let v be Element of (Polynom-Ring (n,L)); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider p = v as Polynomial of n,L by Def10; reconsider w = - p as Element of (Polynom-Ring (n,L)) by Def10; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (Polynom-Ring (n,L)) thus v + w = p - p by Def10 .= 0_ (n,L) by Th24 .= 0. (Polynom-Ring (n,L)) by Def10 ; ::_thesis: verum end; end; registration let n be Ordinal; let L be non empty non trivial right_complementable commutative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring (n,L) -> non empty strict commutative ; coherence Polynom-Ring (n,L) is commutative proof set Pm = Polynom-Ring (n,L); let v, w be Element of (Polynom-Ring (n,L)); :: according to GROUP_1:def_12 ::_thesis: v * w = w * v reconsider p = v, q = w as Polynomial of n,L by Def10; thus v * w = q *' p by Def10 .= w * v by Def10 ; ::_thesis: verum end; end; registration let n be Ordinal; let L be non empty non trivial right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring (n,L) -> non empty strict associative ; coherence Polynom-Ring (n,L) is associative proof set Pm = Polynom-Ring (n,L); let x, y, z be Element of (Polynom-Ring (n,L)); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) reconsider p = x, q = y, r = z as Polynomial of n,L by Def10; A1: y * z = q *' r by Def10; x * y = p *' q by Def10; hence (x * y) * z = (p *' q) *' r by Def10 .= p *' (q *' r) by Th27 .= x * (y * z) by A1, Def10 ; ::_thesis: verum end; end; Lm1: now__::_thesis:_for_n_being_Ordinal for_L_being_non_empty_non_trivial_right_complementable_associative_well-unital_distributive_Abelian_add-associative_right_zeroed_doubleLoopStr_ for_x,_e_being_Element_of_(Polynom-Ring_(n,L))_st_e_=_1._(Polynom-Ring_(n,L))_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let n be Ordinal; ::_thesis: for L being non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds ( x * e = x & e * x = x ) let L be non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds ( x * e = x & e * x = x ) set Pm = Polynom-Ring (n,L); let x, e be Element of (Polynom-Ring (n,L)); ::_thesis: ( e = 1. (Polynom-Ring (n,L)) implies ( x * e = x & e * x = x ) ) reconsider p = x as Polynomial of n,L by Def10; assume A1: e = 1. (Polynom-Ring (n,L)) ; ::_thesis: ( x * e = x & e * x = x ) A2: 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def10; hence x * e = p *' (1_ (n,L)) by A1, Def10 .= x by Th29 ; ::_thesis: e * x = x thus e * x = (1_ (n,L)) *' p by A1, A2, Def10 .= x by Th30 ; ::_thesis: verum end; registration let n be Ordinal; let L be non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring (n,L) -> non empty strict right-distributive well-unital ; coherence ( Polynom-Ring (n,L) is well-unital & Polynom-Ring (n,L) is right-distributive ) proof set Pm = Polynom-Ring (n,L); thus Polynom-Ring (n,L) is well-unital ::_thesis: Polynom-Ring (n,L) is right-distributive proof let x be Element of (Polynom-Ring (n,L)); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (Polynom-Ring (n,L))) = x & (1. (Polynom-Ring (n,L))) * x = x ) thus ( x * (1. (Polynom-Ring (n,L))) = x & (1. (Polynom-Ring (n,L))) * x = x ) by Lm1; ::_thesis: verum end; let x, y, z be Element of (Polynom-Ring (n,L)); :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z) reconsider p = x, q = y, r = z as Polynomial of n,L by Def10; A1: ( x * y = p *' q & x * z = p *' r ) by Def10; y + z = q + r by Def10; hence x * (y + z) = p *' (q + r) by Def10 .= (p *' q) + (p *' r) by Th26 .= (x * y) + (x * z) by A1, Def10 ; ::_thesis: verum end; end; theorem :: POLYNOM1:31 for n being Ordinal for L being non empty non trivial right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr holds 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def10;