:: POLYNOM3 semantic presentation begin theorem Th1: :: POLYNOM3:1 for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds p . i = 0. L ) holds Sum p = 0. L proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds p . i = 0. L ) holds Sum p = 0. L let p be FinSequence of the carrier of L; ::_thesis: ( ( for i being Element of NAT st i in dom p holds p . i = 0. L ) implies Sum p = 0. L ) assume A1: for k being Element of NAT st k in dom p holds p . k = 0. L ; ::_thesis: Sum p = 0. L now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_ p_/._k_=_0._L let k be Nat; ::_thesis: ( k in dom p implies p /. k = 0. L ) assume A2: k in dom p ; ::_thesis: p /. k = 0. L hence p /. k = p . k by PARTFUN1:def_6 .= 0. L by A1, A2 ; ::_thesis: verum end; hence Sum p = 0. L by MATRLIN:11; ::_thesis: verum end; theorem Th2: :: POLYNOM3:2 for V being non empty Abelian add-associative right_zeroed addLoopStr for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p) proof let V be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p) defpred S1[ FinSequence of the carrier of V] means Sum $1 = Sum (Rev $1); A1: for p being FinSequence of the carrier of V for x being Element of V st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of the carrier of V; ::_thesis: for x being Element of V st S1[p] holds S1[p ^ <*x*>] let x be Element of V; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A2: Sum p = Sum (Rev p) ; ::_thesis: S1[p ^ <*x*>] thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41 .= Sum (<*x*> ^ (Rev p)) by A2, RLVECT_1:41 .= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; ::_thesis: verum end; A3: S1[ <*> the carrier of V] ; thus for p being FinSequence of the carrier of V holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum end; theorem Th3: :: POLYNOM3:3 for p being FinSequence of REAL holds Sum p = Sum (Rev p) proof defpred S1[ FinSequence of REAL ] means Sum $1 = Sum (Rev $1); A1: for p being FinSequence of REAL for x being Element of REAL st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S1[p] holds S1[p ^ <*x*>] let x be Element of REAL ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A2: Sum p = Sum (Rev p) ; ::_thesis: S1[p ^ <*x*>] thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RVSUM_1:75 .= Sum (<*x*> ^ (Rev p)) by A2, RVSUM_1:75 .= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; ::_thesis: verum end; A3: S1[ <*> REAL] ; thus for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum end; theorem Th4: :: POLYNOM3:4 for p being FinSequence of NAT for i being Element of NAT st i in dom p holds Sum p >= p . i proof defpred S1[ FinSequence of NAT ] means for i being Element of NAT st i in dom $1 holds Sum $1 >= $1 . i; A1: for p being FinSequence of NAT for x being Element of NAT st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of NAT ; ::_thesis: for x being Element of NAT st S1[p] holds S1[p ^ <*x*>] let x be Element of NAT ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A2: for i being Element of NAT st i in dom p holds Sum p >= p . i ; ::_thesis: S1[p ^ <*x*>] let i be Element of NAT ; ::_thesis: ( i in dom (p ^ <*x*>) implies Sum (p ^ <*x*>) >= (p ^ <*x*>) . i ) A3: (p . i) + x >= p . i by NAT_1:11; len (p ^ <*x*>) = (len p) + 1 by FINSEQ_2:16; then A4: dom (p ^ <*x*>) = Seg ((len p) + 1) by FINSEQ_1:def_3 .= (Seg (len p)) \/ {((len p) + 1)} by FINSEQ_1:9 .= (dom p) \/ {((len p) + 1)} by FINSEQ_1:def_3 ; assume A5: i in dom (p ^ <*x*>) ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i percases ( i in dom p or i in {((len p) + 1)} ) by A5, A4, XBOOLE_0:def_3; supposeA6: i in dom p ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i then Sum p >= p . i by A2; then (Sum p) + x >= (p . i) + x by XREAL_1:6; then Sum (p ^ <*x*>) >= (p . i) + x by RVSUM_1:74; then Sum (p ^ <*x*>) >= p . i by A3, XXREAL_0:2; hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by A6, FINSEQ_1:def_7; ::_thesis: verum end; suppose i in {((len p) + 1)} ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i then i = (len p) + 1 by TARSKI:def_1; then (p ^ <*x*>) . i = x by FINSEQ_1:42; then (Sum p) + x >= (p ^ <*x*>) . i by NAT_1:11; hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by RVSUM_1:74; ::_thesis: verum end; end; end; A7: S1[ <*> NAT] ; thus for p being FinSequence of NAT holds S1[p] from FINSEQ_2:sch_2(A7, A1); ::_thesis: verum end; definition let D be non empty set ; let i be Element of NAT ; let p be FinSequence of D; :: original: Del redefine func Del (p,i) -> FinSequence of D; coherence Del (p,i) is FinSequence of D by FINSEQ_3:105; end; definition let D be non empty set ; let a, b be Element of D; :: original: <* redefine func<*a,b*> -> Element of 2 -tuples_on D; coherence <*a,b*> is Element of 2 -tuples_on D by FINSEQ_2:101; end; definition let D be non empty set ; let k, n be Element of NAT ; let p be Element of k -tuples_on D; let q be Element of n -tuples_on D; :: original: ^ redefine funcp ^ q -> Element of (k + n) -tuples_on D; coherence p ^ q is Element of (k + n) -tuples_on D proof p ^ q is Tuple of k + n,D ; hence p ^ q is Element of (k + n) -tuples_on D by FINSEQ_2:131; ::_thesis: verum end; end; definition let D be non empty set ; let k, n be Element of NAT ; let p be FinSequence of k -tuples_on D; let q be FinSequence of n -tuples_on D; :: original: ^^ redefine funcp ^^ q -> Element of ((k + n) -tuples_on D) * ; coherence p ^^ q is Element of ((k + n) -tuples_on D) * proof rng (p ^^ q) c= (k + n) -tuples_on D proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p ^^ q) or y in (k + n) -tuples_on D ) assume y in rng (p ^^ q) ; ::_thesis: y in (k + n) -tuples_on D then consider x being set such that A1: x in dom (p ^^ q) and A2: y = (p ^^ q) . x by FUNCT_1:def_3; A3: x in (dom p) /\ (dom q) by A1, PRE_POLY:def_4; then A4: x in dom p by XBOOLE_0:def_4; A5: x in dom q by A3, XBOOLE_0:def_4; y = (p . x) ^ (q . x) by A1, A2, PRE_POLY:def_4 .= (p /. x) ^ (q . x) by A4, PARTFUN1:def_6 .= (p /. x) ^ (q /. x) by A5, PARTFUN1:def_6 ; hence y in (k + n) -tuples_on D ; ::_thesis: verum end; then p ^^ q is FinSequence of (k + n) -tuples_on D by FINSEQ_1:def_4; hence p ^^ q is Element of ((k + n) -tuples_on D) * by FINSEQ_1:def_11; ::_thesis: verum end; end; scheme :: POLYNOM3:sch 1 SeqOfSeqLambdaD{ F1() -> non empty set , F2() -> Element of NAT , F3( Element of NAT ) -> Element of NAT , F4( set , set ) -> Element of F1() } : ex p being FinSequence of F1() * st ( len p = F2() & ( for k being Element of NAT st k in Seg F2() holds ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds (p /. k) . n = F4(k,n) ) ) ) ) proof defpred S1[ Element of NAT , FinSequence] means ( len $2 = F3($1) & ( for n being Element of NAT st n in dom $2 holds $2 . n = F4($1,n) ) ); A1: for k being Element of NAT st k in Seg F2() holds ex d being Element of F1() * st S1[k,d] proof let k be Element of NAT ; ::_thesis: ( k in Seg F2() implies ex d being Element of F1() * st S1[k,d] ) assume k in Seg F2() ; ::_thesis: ex d being Element of F1() * st S1[k,d] deffunc H1( Nat) -> Element of F1() = F4(k,$1); consider d being FinSequence of F1() such that A2: len d = F3(k) and A3: for n being Nat st n in dom d holds d . n = H1(n) from FINSEQ_2:sch_1(); reconsider d = d as Element of F1() * by FINSEQ_1:def_11; take d ; ::_thesis: S1[k,d] thus len d = F3(k) by A2; ::_thesis: for n being Element of NAT st n in dom d holds d . n = F4(k,n) let n be Element of NAT ; ::_thesis: ( n in dom d implies d . n = F4(k,n) ) assume n in dom d ; ::_thesis: d . n = F4(k,n) hence d . n = F4(k,n) by A3; ::_thesis: verum end; consider p being FinSequence of F1() * such that A4: dom p = Seg F2() and A5: for k being Element of NAT st k in Seg F2() holds S1[k,p /. k] from RECDEF_1:sch_17(A1); take p ; ::_thesis: ( len p = F2() & ( for k being Element of NAT st k in Seg F2() holds ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds (p /. k) . n = F4(k,n) ) ) ) ) thus len p = F2() by A4, FINSEQ_1:def_3; ::_thesis: for k being Element of NAT st k in Seg F2() holds ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds (p /. k) . n = F4(k,n) ) ) let k be Element of NAT ; ::_thesis: ( k in Seg F2() implies ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds (p /. k) . n = F4(k,n) ) ) ) assume k in Seg F2() ; ::_thesis: ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds (p /. k) . n = F4(k,n) ) ) hence ( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds (p /. k) . n = F4(k,n) ) ) by A5; ::_thesis: verum end; begin definition let n be Element of NAT ; let p, q be Element of n -tuples_on NAT; predp < q means :Def1: :: POLYNOM3:def 1 ex i being Element of NAT st ( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ); asymmetry for p, q being Element of n -tuples_on NAT st ex i being Element of NAT st ( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) holds for i being Element of NAT holds ( not i in Seg n or not q . i < p . i or ex k being Element of NAT st ( 1 <= k & k < i & not q . k = p . k ) ) proof let p, q be Element of n -tuples_on NAT; ::_thesis: ( ex i being Element of NAT st ( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) implies for i being Element of NAT holds ( not i in Seg n or not q . i < p . i or ex k being Element of NAT st ( 1 <= k & k < i & not q . k = p . k ) ) ) given i being Element of NAT such that A1: i in Seg n and A2: p . i < q . i and A3: for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ; ::_thesis: for i being Element of NAT holds ( not i in Seg n or not q . i < p . i or ex k being Element of NAT st ( 1 <= k & k < i & not q . k = p . k ) ) A4: 1 <= i by A1, FINSEQ_1:1; given j being Element of NAT such that A5: j in Seg n and A6: q . j < p . j and A7: for k being Element of NAT st 1 <= k & k < j holds q . k = p . k ; ::_thesis: contradiction A8: 1 <= j by A5, FINSEQ_1:1; percases ( i < j or j < i or i = j ) by XXREAL_0:1; suppose i < j ; ::_thesis: contradiction hence contradiction by A2, A7, A4; ::_thesis: verum end; suppose j < i ; ::_thesis: contradiction hence contradiction by A3, A6, A8; ::_thesis: verum end; suppose i = j ; ::_thesis: contradiction hence contradiction by A2, A6; ::_thesis: verum end; end; end; end; :: deftheorem Def1 defines < POLYNOM3:def_1_:_ for n being Element of NAT for p, q being Element of n -tuples_on NAT holds ( p < q iff ex i being Element of NAT st ( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) ); notation let n be Element of NAT ; let p, q be Element of n -tuples_on NAT; synonym q > p for p < q; end; definition let n be Element of NAT ; let p, q be Element of n -tuples_on NAT; predp <= q means :Def2: :: POLYNOM3:def 2 ( p < q or p = q ); reflexivity for p being Element of n -tuples_on NAT holds ( p < p or p = p ) ; end; :: deftheorem Def2 defines <= POLYNOM3:def_2_:_ for n being Element of NAT for p, q being Element of n -tuples_on NAT holds ( p <= q iff ( p < q or p = q ) ); notation let n be Element of NAT ; let p, q be Element of n -tuples_on NAT; synonym q >= p for p <= q; end; theorem Th5: :: POLYNOM3:5 for n being Element of NAT for p, q, r being Element of n -tuples_on NAT holds ( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) ) proof let n be Element of NAT ; ::_thesis: for p, q, r being Element of n -tuples_on NAT holds ( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) ) let p, q, r be Element of n -tuples_on NAT; ::_thesis: ( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) ) thus A1: ( p < q & q < r implies p < r ) ::_thesis: ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) proof assume that A2: p < q and A3: q < r ; ::_thesis: p < r consider i being Element of NAT such that A4: i in Seg n and A5: p . i < q . i and A6: for k being Element of NAT st 1 <= k & k < i holds p . k = q . k by A2, Def1; consider j being Element of NAT such that A7: j in Seg n and A8: q . j < r . j and A9: for k being Element of NAT st 1 <= k & k < j holds q . k = r . k by A3, Def1; reconsider t = min (i,j) as Element of NAT ; take t ; :: according to POLYNOM3:def_1 ::_thesis: ( t in Seg n & p . t < r . t & ( for k being Element of NAT st 1 <= k & k < t holds p . k = r . k ) ) thus t in Seg n by A4, A7, XXREAL_0:15; ::_thesis: ( p . t < r . t & ( for k being Element of NAT st 1 <= k & k < t holds p . k = r . k ) ) now__::_thesis:_p_._t_<_r_._t percases ( i < j or i > j or i = j ) by XXREAL_0:1; supposeA10: i < j ; ::_thesis: p . t < r . t A11: i >= 1 by A4, FINSEQ_1:1; t = i by A10, XXREAL_0:def_9; hence p . t < r . t by A5, A9, A10, A11; ::_thesis: verum end; supposeA12: i > j ; ::_thesis: p . t < r . t A13: j >= 1 by A7, FINSEQ_1:1; t = j by A12, XXREAL_0:def_9; hence p . t < r . t by A6, A8, A12, A13; ::_thesis: verum end; suppose i = j ; ::_thesis: p . t < r . t hence p . t < r . t by A5, A8, XXREAL_0:2; ::_thesis: verum end; end; end; hence p . t < r . t ; ::_thesis: for k being Element of NAT st 1 <= k & k < t holds p . k = r . k let k be Element of NAT ; ::_thesis: ( 1 <= k & k < t implies p . k = r . k ) assume that A14: 1 <= k and A15: k < t ; ::_thesis: p . k = r . k t <= j by XXREAL_0:17; then A16: k < j by A15, XXREAL_0:2; t <= i by XXREAL_0:17; then k < i by A15, XXREAL_0:2; hence p . k = q . k by A6, A14 .= r . k by A9, A14, A16 ; ::_thesis: verum end; assume A17: ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) ; ::_thesis: p <= r percases ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) by A17; supposeA18: ( p < q & q <= r ) ; ::_thesis: p <= r then ( q < r or q = r ) by Def2; hence p <= r by A1, A18, Def2; ::_thesis: verum end; supposeA19: ( p <= q & q < r ) ; ::_thesis: p <= r then ( p < q or p = q ) by Def2; hence p <= r by A1, A19, Def2; ::_thesis: verum end; suppose ( p <= q & q <= r ) ; ::_thesis: p <= r hence p <= r by A1, Def2; ::_thesis: verum end; end; end; theorem Th6: :: POLYNOM3:6 for n being Element of NAT for p, q being Element of n -tuples_on NAT st p <> q holds ex i being Element of NAT st ( i in Seg n & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) proof defpred S1[ Nat] means for p, q being Element of $1 -tuples_on NAT st p <> q holds ex i being Element of NAT st ( i in Seg $1 & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: for p, q being Element of n -tuples_on NAT st p <> q holds ex i being Element of NAT st ( i in Seg n & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) ; ::_thesis: S1[n + 1] let p, q be Element of (n + 1) -tuples_on NAT; ::_thesis: ( p <> q implies ex i being Element of NAT st ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) ) consider t1 being Element of n -tuples_on NAT, d1 being Element of NAT such that A3: p = t1 ^ <*d1*> by FINSEQ_2:117; assume A4: p <> q ; ::_thesis: ex i being Element of NAT st ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) consider t2 being Element of n -tuples_on NAT, d2 being Element of NAT such that A5: q = t2 ^ <*d2*> by FINSEQ_2:117; A6: len t1 = n by CARD_1:def_7; A7: len t2 = n by CARD_1:def_7; percases ( t1 <> t2 or t1 = t2 ) ; suppose t1 <> t2 ; ::_thesis: ex i being Element of NAT st ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) then consider i being Element of NAT such that A8: i in Seg n and A9: t1 . i <> t2 . i and A10: for k being Element of NAT st 1 <= k & k < i holds t1 . k = t2 . k by A2; take i ; ::_thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) thus i in Seg (n + 1) by A8, FINSEQ_2:8; ::_thesis: ( p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) i in dom t1 by A6, A8, FINSEQ_1:def_3; then A11: p . i = t1 . i by A3, FINSEQ_1:def_7; i in dom t2 by A7, A8, FINSEQ_1:def_3; hence p . i <> q . i by A5, A9, A11, FINSEQ_1:def_7; ::_thesis: for k being Element of NAT st 1 <= k & k < i holds p . k = q . k let k be Element of NAT ; ::_thesis: ( 1 <= k & k < i implies p . k = q . k ) assume that A12: 1 <= k and A13: k < i ; ::_thesis: p . k = q . k i <= n by A8, FINSEQ_1:1; then A14: k <= n by A13, XXREAL_0:2; then A15: k in dom t1 by A6, A12, FINSEQ_3:25; A16: k in dom t2 by A7, A12, A14, FINSEQ_3:25; t1 . k = t2 . k by A10, A12, A13; hence p . k = t2 . k by A3, A15, FINSEQ_1:def_7 .= q . k by A5, A16, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA17: t1 = t2 ; ::_thesis: ex i being Element of NAT st ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) take i = n + 1; ::_thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) thus i in Seg (n + 1) by FINSEQ_1:4; ::_thesis: ( p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds p . k = q . k ) ) p . i = d1 by A3, FINSEQ_2:116; hence p . i <> q . i by A3, A5, A4, A17, FINSEQ_2:116; ::_thesis: for k being Element of NAT st 1 <= k & k < i holds p . k = q . k let k be Element of NAT ; ::_thesis: ( 1 <= k & k < i implies p . k = q . k ) assume that A18: 1 <= k and A19: k < i ; ::_thesis: p . k = q . k A20: k <= n by A19, NAT_1:13; then A21: k in dom t2 by A7, A18, FINSEQ_3:25; k in dom t1 by A6, A18, A20, FINSEQ_3:25; hence p . k = t2 . k by A3, A17, FINSEQ_1:def_7 .= q . k by A5, A21, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; A22: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A22, A1); ::_thesis: verum end; theorem Th7: :: POLYNOM3:7 for n being Element of NAT for p, q being Element of n -tuples_on NAT holds ( p <= q or p > q ) proof let n be Element of NAT ; ::_thesis: for p, q being Element of n -tuples_on NAT holds ( p <= q or p > q ) let p, q be Element of n -tuples_on NAT; ::_thesis: ( p <= q or p > q ) assume A1: not p <= q ; ::_thesis: p > q then consider i being Element of NAT such that A2: i in Seg n and A3: p . i <> q . i and A4: for k being Element of NAT st 1 <= k & k < i holds p . k = q . k by Th6; take i ; :: according to POLYNOM3:def_1 ::_thesis: ( i in Seg n & q . i < p . i & ( for k being Element of NAT st 1 <= k & k < i holds q . k = p . k ) ) thus i in Seg n by A2; ::_thesis: ( q . i < p . i & ( for k being Element of NAT st 1 <= k & k < i holds q . k = p . k ) ) not p < q by A1, Def2; then p . i >= q . i by A2, A4, Def1; hence q . i < p . i by A3, XXREAL_0:1; ::_thesis: for k being Element of NAT st 1 <= k & k < i holds q . k = p . k thus for k being Element of NAT st 1 <= k & k < i holds q . k = p . k by A4; ::_thesis: verum end; definition let n be Element of NAT ; func TuplesOrder n -> Order of (n -tuples_on NAT) means :Def3: :: POLYNOM3:def 3 for p, q being Element of n -tuples_on NAT holds ( [p,q] in it iff p <= q ); existence ex b1 being Order of (n -tuples_on NAT) st for p, q being Element of n -tuples_on NAT holds ( [p,q] in b1 iff p <= q ) proof defpred S1[ Element of n -tuples_on NAT, Element of n -tuples_on NAT] means $1 <= $2; consider R being Relation of (n -tuples_on NAT),(n -tuples_on NAT) such that A1: for x, y being Element of n -tuples_on NAT holds ( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2(); A2: R is_transitive_in n -tuples_on NAT proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in n -tuples_on NAT or not y in n -tuples_on NAT or not z in n -tuples_on NAT or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume that A3: ( x in n -tuples_on NAT & y in n -tuples_on NAT & z in n -tuples_on NAT ) and A4: ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R reconsider x1 = x, y1 = y, z1 = z as Element of n -tuples_on NAT by A3; ( x1 <= y1 & y1 <= z1 ) by A1, A4; then x1 <= z1 by Th5; hence [x,z] in R by A1; ::_thesis: verum end; A5: R is_reflexive_in n -tuples_on NAT proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in n -tuples_on NAT or [x,x] in R ) assume x in n -tuples_on NAT ; ::_thesis: [x,x] in R then reconsider x1 = x as Element of n -tuples_on NAT ; x1 <= x1 ; hence [x,x] in R by A1; ::_thesis: verum end; then A6: ( dom R = n -tuples_on NAT & field R = n -tuples_on NAT ) by ORDERS_1:13; R is_antisymmetric_in n -tuples_on NAT proof let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in n -tuples_on NAT or not y in n -tuples_on NAT or not [x,y] in R or not [y,x] in R or x = y ) assume that A7: ( x in n -tuples_on NAT & y in n -tuples_on NAT ) and A8: [x,y] in R and A9: [y,x] in R ; ::_thesis: x = y reconsider x1 = x, y1 = y as Element of n -tuples_on NAT by A7; x1 <= y1 by A1, A8; then A10: ( x1 < y1 or x1 = y1 ) by Def2; y1 <= x1 by A1, A9; hence x = y by A10, Def2; ::_thesis: verum end; then reconsider R = R as Order of (n -tuples_on NAT) by A5, A2, A6, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; take R ; ::_thesis: for p, q being Element of n -tuples_on NAT holds ( [p,q] in R iff p <= q ) thus for p, q being Element of n -tuples_on NAT holds ( [p,q] in R iff p <= q ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Order of (n -tuples_on NAT) st ( for p, q being Element of n -tuples_on NAT holds ( [p,q] in b1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds ( [p,q] in b2 iff p <= q ) ) holds b1 = b2 proof let T1, T2 be Order of (n -tuples_on NAT); ::_thesis: ( ( for p, q being Element of n -tuples_on NAT holds ( [p,q] in T1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds ( [p,q] in T2 iff p <= q ) ) implies T1 = T2 ) assume that A11: for p, q being Element of n -tuples_on NAT holds ( [p,q] in T1 iff p <= q ) and A12: for p, q being Element of n -tuples_on NAT holds ( [p,q] in T2 iff p <= q ) ; ::_thesis: T1 = T2 let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in T1 or [x,y] in T2 ) & ( not [x,y] in T2 or [x,y] in T1 ) ) thus ( [x,y] in T1 implies [x,y] in T2 ) ::_thesis: ( not [x,y] in T2 or [x,y] in T1 ) proof assume A13: [x,y] in T1 ; ::_thesis: [x,y] in T2 then consider p, q being set such that A14: [x,y] = [p,q] and A15: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2; reconsider p = p, q = q as Element of n -tuples_on NAT by A15; p <= q by A11, A13, A14; hence [x,y] in T2 by A12, A14; ::_thesis: verum end; assume A16: [x,y] in T2 ; ::_thesis: [x,y] in T1 then consider p, q being set such that A17: [x,y] = [p,q] and A18: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2; reconsider p = p, q = q as Element of n -tuples_on NAT by A18; p <= q by A12, A16, A17; hence [x,y] in T1 by A11, A17; ::_thesis: verum end; end; :: deftheorem Def3 defines TuplesOrder POLYNOM3:def_3_:_ for n being Element of NAT for b2 being Order of (n -tuples_on NAT) holds ( b2 = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds ( [p,q] in b2 iff p <= q ) ); registration let n be Element of NAT ; cluster TuplesOrder n -> being_linear-order ; coherence TuplesOrder n is being_linear-order proof now__::_thesis:_for_x,_y_being_set_st_x_in_n_-tuples_on_NAT_&_y_in_n_-tuples_on_NAT_&_x_<>_y_&_not_[x,y]_in_TuplesOrder_n_holds_ [y,x]_in_TuplesOrder_n let x, y be set ; ::_thesis: ( x in n -tuples_on NAT & y in n -tuples_on NAT & x <> y & not [x,y] in TuplesOrder n implies [y,x] in TuplesOrder n ) assume that A1: ( x in n -tuples_on NAT & y in n -tuples_on NAT ) and x <> y and A2: not [x,y] in TuplesOrder n ; ::_thesis: [y,x] in TuplesOrder n reconsider p = x, q = y as Element of n -tuples_on NAT by A1; not p <= q by A2, Def3; then p > q by Th7; then q <= p by Def2; hence [y,x] in TuplesOrder n by Def3; ::_thesis: verum end; then ( field (TuplesOrder n) = n -tuples_on NAT & TuplesOrder n is_connected_in n -tuples_on NAT ) by ORDERS_1:15, RELAT_2:def_6; then TuplesOrder n is connected by RELAT_2:def_14; hence TuplesOrder n is being_linear-order by ORDERS_1:def_5; ::_thesis: verum end; end; begin definition let i be non empty Element of NAT ; let n be Element of NAT ; func Decomp (n,i) -> FinSequence of i -tuples_on NAT means :Def4: :: POLYNOM3:def 4 ex A being finite Subset of (i -tuples_on NAT) st ( it = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ); existence ex b1 being FinSequence of i -tuples_on NAT ex A being finite Subset of (i -tuples_on NAT) st ( b1 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) proof reconsider n1 = n + 1 as non empty set ; defpred S1[ Element of i -tuples_on NAT] means Sum $1 = n; consider A being Subset of (i -tuples_on NAT) such that A1: for p being Element of i -tuples_on NAT holds ( p in A iff S1[p] ) from SUBSET_1:sch_3(); A2: A c= i -tuples_on (n + 1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in i -tuples_on (n + 1) ) assume A3: x in A ; ::_thesis: x in i -tuples_on (n + 1) then reconsider p = x as Element of i -tuples_on NAT ; A4: Sum p = n by A1, A3; rng p c= n + 1 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in n + 1 ) assume that A5: y in rng p and A6: not y in n + 1 ; ::_thesis: contradiction rng p c= NAT by FINSEQ_1:def_4; then reconsider k = y as Element of NAT by A5; not y in { t where t is Element of NAT : t < n + 1 } by A6, AXIOMS:4; then A7: k >= n + 1 ; ex j being Nat st ( j in dom p & p . j = k ) by A5, FINSEQ_2:10; then Sum p >= k by Th4; hence contradiction by A4, A7, NAT_1:13; ::_thesis: verum end; then ( len p = i & p is FinSequence of n + 1 ) by CARD_1:def_7, FINSEQ_1:def_4; then p is Element of i -tuples_on n1 by FINSEQ_2:92; hence x in i -tuples_on (n + 1) ; ::_thesis: verum end; reconsider A = A as finite Subset of (i -tuples_on NAT) by A2; take SgmX ((TuplesOrder i),A) ; ::_thesis: ex A being finite Subset of (i -tuples_on NAT) st ( SgmX ((TuplesOrder i),A) = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) thus ex A being finite Subset of (i -tuples_on NAT) st ( SgmX ((TuplesOrder i),A) = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of i -tuples_on NAT st ex A being finite Subset of (i -tuples_on NAT) st ( b1 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT) st ( b2 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) holds b1 = b2 proof let p1, p2 be FinSequence of i -tuples_on NAT; ::_thesis: ( ex A being finite Subset of (i -tuples_on NAT) st ( p1 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT) st ( p2 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) implies p1 = p2 ) given A1 being finite Subset of (i -tuples_on NAT) such that A8: p1 = SgmX ((TuplesOrder i),A1) and A9: for p being Element of i -tuples_on NAT holds ( p in A1 iff Sum p = n ) ; ::_thesis: ( for A being finite Subset of (i -tuples_on NAT) holds ( not p2 = SgmX ((TuplesOrder i),A) or ex p being Element of i -tuples_on NAT st ( ( p in A implies Sum p = n ) implies ( Sum p = n & not p in A ) ) ) or p1 = p2 ) given A2 being finite Subset of (i -tuples_on NAT) such that A10: p2 = SgmX ((TuplesOrder i),A2) and A11: for p being Element of i -tuples_on NAT holds ( p in A2 iff Sum p = n ) ; ::_thesis: p1 = p2 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_A1_implies_x_in_A2_)_&_(_x_in_A2_implies_x_in_A1_)_) let x be set ; ::_thesis: ( ( x in A1 implies x in A2 ) & ( x in A2 implies x in A1 ) ) thus ( x in A1 implies x in A2 ) ::_thesis: ( x in A2 implies x in A1 ) proof assume A12: x in A1 ; ::_thesis: x in A2 then reconsider p = x as Element of i -tuples_on NAT ; Sum p = n by A9, A12; hence x in A2 by A11; ::_thesis: verum end; assume A13: x in A2 ; ::_thesis: x in A1 then reconsider p = x as Element of i -tuples_on NAT ; Sum p = n by A11, A13; hence x in A1 by A9; ::_thesis: verum end; hence p1 = p2 by A8, A10, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def4 defines Decomp POLYNOM3:def_4_:_ for i being non empty Element of NAT for n being Element of NAT for b3 being FinSequence of i -tuples_on NAT holds ( b3 = Decomp (n,i) iff ex A being finite Subset of (i -tuples_on NAT) st ( b3 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) ) ) ); registration let i be non empty Element of NAT ; let n be Element of NAT ; cluster Decomp (n,i) -> one-to-one non empty FinSequence-yielding ; coherence ( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding ) proof reconsider p2 = (i -' 1) |-> 0 as FinSequence of NAT ; i >= 1 by NAT_1:14; then (i -' 1) + 1 = i by XREAL_1:235; then ((i -' 1) |-> 0) ^ <*n*> is Tuple of i, NAT ; then reconsider p1 = ((i -' 1) |-> 0) ^ <*n*> as Element of i -tuples_on NAT by FINSEQ_2:131; consider A being finite Subset of (i -tuples_on NAT) such that A1: Decomp (n,i) = SgmX ((TuplesOrder i),A) and A2: for p being Element of i -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; Sum p1 = (Sum p2) + n by RVSUM_1:74 .= 0 + n by RVSUM_1:81 ; then reconsider A = A as non empty finite Subset of (i -tuples_on NAT) by A2; ( not SgmX ((TuplesOrder i),A) is empty & SgmX ((TuplesOrder i),A) is finite ) ; hence ( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding ) by A1; ::_thesis: verum end; end; theorem Th8: :: POLYNOM3:8 for n being Element of NAT holds len (Decomp (n,1)) = 1 proof let n be Element of NAT ; ::_thesis: len (Decomp (n,1)) = 1 consider A being finite Subset of (1 -tuples_on NAT) such that A1: Decomp (n,1) = SgmX ((TuplesOrder 1),A) and A2: for p being Element of 1 -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; A3: A = {<*n*>} proof thus A c= {<*n*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*n*>} c= A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in {<*n*>} ) assume A4: y in A ; ::_thesis: y in {<*n*>} then reconsider p = y as Element of 1 -tuples_on NAT ; A5: Sum p = n by A2, A4; consider k being Element of NAT such that A6: p = <*k*> by FINSEQ_2:97; Sum p = k by A6, RVSUM_1:73; hence y in {<*n*>} by A5, A6, TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {<*n*>} or y in A ) assume y in {<*n*>} ; ::_thesis: y in A then A7: y = <*n*> by TARSKI:def_1; A8: <*n*> is Element of 1 -tuples_on NAT by FINSEQ_2:131; Sum <*n*> = n by RVSUM_1:73; hence y in A by A2, A7, A8; ::_thesis: verum end; field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:15; then TuplesOrder 1 linearly_orders 1 -tuples_on NAT by ORDERS_1:37; hence len (Decomp (n,1)) = card A by A1, ORDERS_1:38, PRE_POLY:11 .= 1 by A3, CARD_1:30 ; ::_thesis: verum end; theorem Th9: :: POLYNOM3:9 for n being Element of NAT holds len (Decomp (n,2)) = n + 1 proof let n be Element of NAT ; ::_thesis: len (Decomp (n,2)) = n + 1 deffunc H1( Nat) -> set = <*$1,(n -' $1)*>; consider q being FinSequence such that A1: len q = n and A2: for k being Nat st k in dom q holds q . k = H1(k) from FINSEQ_1:sch_2(); A3: dom q = Seg n by A1, FINSEQ_1:def_3; set q1 = q ^ <*<*0,n*>*>; A4: dom q = Seg n by A1, FINSEQ_1:def_3; A5: len (q ^ <*<*0,n*>*>) = n + 1 by A1, FINSEQ_2:16; then A6: dom (q ^ <*<*0,n*>*>) = Seg (n + 1) by FINSEQ_1:def_3; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(q_^_<*<*0,n*>*>)_&_x2_in_dom_(q_^_<*<*0,n*>*>)_&_(q_^_<*<*0,n*>*>)_._x1_=_(q_^_<*<*0,n*>*>)_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom (q ^ <*<*0,n*>*>) & x2 in dom (q ^ <*<*0,n*>*>) & (q ^ <*<*0,n*>*>) . x1 = (q ^ <*<*0,n*>*>) . x2 implies x1 = x2 ) assume that A7: x1 in dom (q ^ <*<*0,n*>*>) and A8: x2 in dom (q ^ <*<*0,n*>*>) and A9: (q ^ <*<*0,n*>*>) . x1 = (q ^ <*<*0,n*>*>) . x2 ; ::_thesis: x1 = x2 reconsider k1 = x1, k2 = x2 as Element of NAT by A7, A8; x2 in (Seg n) \/ {(n + 1)} by A6, A8, FINSEQ_1:9; then A10: ( x2 in Seg n or x2 in {(n + 1)} ) by XBOOLE_0:def_3; x1 in (Seg n) \/ {(n + 1)} by A6, A7, FINSEQ_1:9; then A11: ( x1 in Seg n or x1 in {(n + 1)} ) by XBOOLE_0:def_3; now__::_thesis:_x1_=_x2 percases ( ( x1 in Seg n & x2 in Seg n ) or ( x1 in Seg n & x2 = n + 1 ) or ( x1 = n + 1 & x2 in Seg n ) or ( x1 = n + 1 & x2 = n + 1 ) ) by A11, A10, TARSKI:def_1; supposeA12: ( x1 in Seg n & x2 in Seg n ) ; ::_thesis: x1 = x2 then A13: ( (q ^ <*<*0,n*>*>) . k1 = q . k1 & (q ^ <*<*0,n*>*>) . k2 = q . k2 ) by A3, FINSEQ_1:def_7; ( q . k1 = <*k1,(n -' k1)*> & q . k2 = <*k2,(n -' k2)*> ) by A2, A4, A12; hence x1 = x2 by A9, A13, FINSEQ_1:77; ::_thesis: verum end; supposeA14: ( x1 in Seg n & x2 = n + 1 ) ; ::_thesis: x1 = x2 then A15: (q ^ <*<*0,n*>*>) . k2 = <*0,n*> by A1, FINSEQ_1:42; (q ^ <*<*0,n*>*>) . k1 = q . k1 by A3, A14, FINSEQ_1:def_7 .= <*k1,(n -' k1)*> by A2, A4, A14 ; then k1 = 0 by A9, A15, FINSEQ_1:77; hence x1 = x2 by A14, FINSEQ_1:1; ::_thesis: verum end; supposeA16: ( x1 = n + 1 & x2 in Seg n ) ; ::_thesis: x1 = x2 then A17: (q ^ <*<*0,n*>*>) . k1 = <*0,n*> by A1, FINSEQ_1:42; (q ^ <*<*0,n*>*>) . k2 = q . k2 by A3, A16, FINSEQ_1:def_7 .= <*k2,(n -' k2)*> by A2, A4, A16 ; then k2 = 0 by A9, A17, FINSEQ_1:77; hence x1 = x2 by A16, FINSEQ_1:1; ::_thesis: verum end; suppose ( x1 = n + 1 & x2 = n + 1 ) ; ::_thesis: x1 = x2 hence x1 = x2 ; ::_thesis: verum end; end; end; hence x1 = x2 ; ::_thesis: verum end; then q ^ <*<*0,n*>*> is one-to-one by FUNCT_1:def_4; then A18: card (rng (q ^ <*<*0,n*>*>)) = n + 1 by A5, FINSEQ_4:62; A19: rng q c= rng (q ^ <*<*0,n*>*>) by FINSEQ_1:29; A20: rng (q ^ <*<*0,n*>*>) = { <*i,(n -' i)*> where i is Element of NAT : i <= n } proof thus rng (q ^ <*<*0,n*>*>) c= { <*i,(n -' i)*> where i is Element of NAT : i <= n } :: according to XBOOLE_0:def_10 ::_thesis: { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= rng (q ^ <*<*0,n*>*>) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (q ^ <*<*0,n*>*>) or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ) assume x in rng (q ^ <*<*0,n*>*>) ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } then consider j being Nat such that A21: j in dom (q ^ <*<*0,n*>*>) and A22: (q ^ <*<*0,n*>*>) . j = x by FINSEQ_2:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; j in (Seg n) \/ {(n + 1)} by A6, A21, FINSEQ_1:9; then A23: ( j in Seg n or j in {(n + 1)} ) by XBOOLE_0:def_3; now__::_thesis:_x_in__{__<*i,(n_-'_i)*>_where_i_is_Element_of_NAT_:_i_<=_n__}_ percases ( j in Seg n or j = n + 1 ) by A23, TARSKI:def_1; supposeA24: j in Seg n ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } then A25: (q ^ <*<*0,n*>*>) . j = q . j by A3, FINSEQ_1:def_7; ( q . j = <*j,(n -' j)*> & j <= n ) by A2, A4, A24, FINSEQ_1:1; hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A22, A25; ::_thesis: verum end; suppose j = n + 1 ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } then (q ^ <*<*0,n*>*>) . j = <*0,n*> by A1, FINSEQ_1:42 .= <*0,(n -' 0)*> by NAT_D:40 ; hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A22; ::_thesis: verum end; end; end; hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } or x in rng (q ^ <*<*0,n*>*>) ) assume x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; ::_thesis: x in rng (q ^ <*<*0,n*>*>) then consider i being Element of NAT such that A26: x = <*i,(n -' i)*> and A27: i <= n ; A28: ( i = 0 or i >= 0 + 1 ) by NAT_1:13; now__::_thesis:_x_in_rng_(q_^_<*<*0,n*>*>) percases ( i = 0 or i in Seg n ) by A27, A28, FINSEQ_1:1; supposeA29: i = 0 ; ::_thesis: x in rng (q ^ <*<*0,n*>*>) A30: n + 1 in dom (q ^ <*<*0,n*>*>) by A6, FINSEQ_1:4; (q ^ <*<*0,n*>*>) . (n + 1) = <*0,n*> by A1, FINSEQ_1:42 .= x by A26, A29, NAT_D:40 ; hence x in rng (q ^ <*<*0,n*>*>) by A30, FUNCT_1:def_3; ::_thesis: verum end; supposeA31: i in Seg n ; ::_thesis: x in rng (q ^ <*<*0,n*>*>) then q . i = x by A2, A4, A26; then x in rng q by A3, A31, FUNCT_1:def_3; hence x in rng (q ^ <*<*0,n*>*>) by A19; ::_thesis: verum end; end; end; hence x in rng (q ^ <*<*0,n*>*>) ; ::_thesis: verum end; consider A being finite Subset of (2 -tuples_on NAT) such that A32: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and A33: for p being Element of 2 -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; A34: A = { <*i,(n -' i)*> where i is Element of NAT : i <= n } proof thus A c= { <*i,(n -' i)*> where i is Element of NAT : i <= n } :: according to XBOOLE_0:def_10 ::_thesis: { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ) assume A35: x in A ; ::_thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } then reconsider p = x as Element of 2 -tuples_on NAT ; consider d1, d2 being Element of NAT such that A36: p = <*d1,d2*> by FINSEQ_2:100; A37: d1 + d2 = Sum p by A36, RVSUM_1:77 .= n by A33, A35 ; then n - d1 >= 0 ; then A38: d2 = n -' d1 by A37, XREAL_0:def_2; d1 <= n by A37, NAT_1:11; hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A36, A38; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } or x in A ) assume x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; ::_thesis: x in A then consider i being Element of NAT such that A39: x = <*i,(n -' i)*> and A40: i <= n ; A41: n - i >= 0 by A40, XREAL_1:48; Sum <*i,(n -' i)*> = i + (n -' i) by RVSUM_1:77 .= i + (n - i) by A41, XREAL_0:def_2 .= n ; hence x in A by A33, A39; ::_thesis: verum end; field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15; then TuplesOrder 2 linearly_orders 2 -tuples_on NAT by ORDERS_1:37; hence len (Decomp (n,2)) = n + 1 by A32, A34, A20, A18, ORDERS_1:38, PRE_POLY:11; ::_thesis: verum end; theorem :: POLYNOM3:10 for n being Element of NAT holds Decomp (n,1) = <*<*n*>*> proof let n be Element of NAT ; ::_thesis: Decomp (n,1) = <*<*n*>*> consider A being finite Subset of (1 -tuples_on NAT) such that A1: Decomp (n,1) = SgmX ((TuplesOrder 1),A) and A2: for p being Element of 1 -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; A3: A = {<*n*>} proof thus A c= {<*n*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*n*>} c= A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in {<*n*>} ) assume A4: y in A ; ::_thesis: y in {<*n*>} then reconsider p = y as Element of 1 -tuples_on NAT ; A5: Sum p = n by A2, A4; consider k being Element of NAT such that A6: p = <*k*> by FINSEQ_2:97; Sum p = k by A6, RVSUM_1:73; hence y in {<*n*>} by A5, A6, TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {<*n*>} or y in A ) assume y in {<*n*>} ; ::_thesis: y in A then A7: y = <*n*> by TARSKI:def_1; A8: <*n*> is Element of 1 -tuples_on NAT by FINSEQ_2:131; Sum <*n*> = n by RVSUM_1:73; hence y in A by A2, A7, A8; ::_thesis: verum end; len (Decomp (n,1)) = 1 by Th8; then A9: dom (Decomp (n,1)) = Seg 1 by FINSEQ_1:def_3 .= dom <*<*n*>*> by FINSEQ_1:38 ; field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:15; then TuplesOrder 1 linearly_orders A by ORDERS_1:37, ORDERS_1:38; then ( rng <*<*n*>*> = {<*n*>} & rng (Decomp (n,1)) = {<*n*>} ) by A1, A3, FINSEQ_1:39, PRE_POLY:def_2; hence Decomp (n,1) = <*<*n*>*> by A9, FUNCT_1:7; ::_thesis: verum end; theorem Th11: :: POLYNOM3:11 for i, j, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> holds ( i < j iff k1 < k2 ) proof let i, j, n, k1, k2 be Element of NAT ; ::_thesis: ( (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> implies ( i < j iff k1 < k2 ) ) assume that A1: (Decomp (n,2)) . i = <*k1,(n -' k1)*> and A2: (Decomp (n,2)) . j = <*k2,(n -' k2)*> ; ::_thesis: ( i < j iff k1 < k2 ) A3: j in dom (Decomp (n,2)) by A2, FUNCT_1:def_2; then A4: (Decomp (n,2)) . j = (Decomp (n,2)) /. j by PARTFUN1:def_6; consider A being finite Subset of (2 -tuples_on NAT) such that A5: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and for p being Element of 2 -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15; then A6: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38; A7: i in dom (Decomp (n,2)) by A1, FUNCT_1:def_2; then A8: (Decomp (n,2)) . i = (Decomp (n,2)) /. i by PARTFUN1:def_6; thus ( i < j implies k1 < k2 ) ::_thesis: ( k1 < k2 implies i < j ) proof assume A9: i < j ; ::_thesis: k1 < k2 then [<*k1,(n -' k1)*>,<*k2,(n -' k2)*>] in TuplesOrder 2 by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def_2; then A10: <*k1,(n -' k1)*> <= <*k2,(n -' k2)*> by Def3; <*k1,(n -' k1)*> <> <*k2,(n -' k2)*> by A5, A6, A1, A2, A7, A3, A8, A4, A9, PRE_POLY:def_2; then <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A10, Def2; then consider t being Element of NAT such that A11: t in Seg 2 and A12: <*k1,(n -' k1)*> . t < <*k2,(n -' k2)*> . t and A13: for k being Element of NAT st 1 <= k & k < t holds <*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k by Def1; percases ( t = 1 or t = 2 ) by A11, FINSEQ_1:2, TARSKI:def_2; supposeA14: t = 1 ; ::_thesis: k1 < k2 then <*k1,(n -' k1)*> . t = k1 by FINSEQ_1:44; hence k1 < k2 by A12, A14, FINSEQ_1:44; ::_thesis: verum end; suppose t = 2 ; ::_thesis: k1 < k2 then <*k1,(n -' k1)*> . 1 = <*k2,(n -' k2)*> . 1 by A13; then <*k1,(n -' k1)*> . 1 = k2 by FINSEQ_1:44; then k1 = k2 by FINSEQ_1:44; hence k1 < k2 by A12; ::_thesis: verum end; end; end; assume A15: k1 < k2 ; ::_thesis: i < j A16: for k being Element of NAT st 1 <= k & k < 1 holds <*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k ; A17: <*k1,(n -' k1)*> . 1 = k1 by FINSEQ_1:44; ( 1 in Seg 2 & <*k2,(n -' k2)*> . 1 = k2 ) by FINSEQ_1:1, FINSEQ_1:44; then A18: <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A15, A17, A16, Def1; assume A19: i >= j ; ::_thesis: contradiction percases ( i = j or j < i ) by A19, XXREAL_0:1; suppose i = j ; ::_thesis: contradiction hence contradiction by A1, A2, A15, A17, FINSEQ_1:44; ::_thesis: verum end; supposeA20: j < i ; ::_thesis: contradiction then [<*k2,(n -' k2)*>,<*k1,(n -' k1)*>] in TuplesOrder 2 by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def_2; then A21: <*k2,(n -' k2)*> <= <*k1,(n -' k1)*> by Def3; <*k2,(n -' k2)*> <> <*k1,(n -' k1)*> by A5, A6, A1, A2, A7, A3, A8, A4, A20, PRE_POLY:def_2; hence contradiction by A18, A21, Def2; ::_thesis: verum end; end; end; theorem Th12: :: POLYNOM3:12 for i, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> holds k2 = k1 + 1 proof let i, n, k1, k2 be Element of NAT ; ::_thesis: ( (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> implies k2 = k1 + 1 ) assume that A1: (Decomp (n,2)) . i = <*k1,(n -' k1)*> and A2: (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> ; ::_thesis: k2 = k1 + 1 assume A3: k2 <> k1 + 1 ; ::_thesis: contradiction i + 0 < i + 1 by XREAL_1:6; then A4: k1 < k2 by A1, A2, Th11; then k1 + 1 <= k2 by NAT_1:13; then A5: k1 + 1 < k2 by A3, XXREAL_0:1; consider A being finite Subset of (2 -tuples_on NAT) such that A6: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and A7: for p being Element of 2 -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15; then TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38; then A8: rng (Decomp (n,2)) = A by A6, PRE_POLY:def_2; k1 < n proof Sum <*k2,(n -' k2)*> = k2 + (n -' k2) by RVSUM_1:77; then A9: Sum <*k2,(n -' k2)*> >= k2 by NAT_1:11; assume k1 >= n ; ::_thesis: contradiction then k2 > n by A4, XXREAL_0:2; then not (Decomp (n,2)) . (i + 1) in rng (Decomp (n,2)) by A7, A8, A2, A9; then not i + 1 in dom (Decomp (n,2)) by FUNCT_1:def_3; hence contradiction by A2, FUNCT_1:def_2; ::_thesis: verum end; then A10: k1 + 1 <= n by NAT_1:13; Sum <*(k1 + 1),(n -' (k1 + 1))*> = (k1 + 1) + (n -' (k1 + 1)) by RVSUM_1:77 .= n by A10, XREAL_1:235 ; then <*(k1 + 1),(n -' (k1 + 1))*> in rng (Decomp (n,2)) by A7, A8; then consider k being Nat such that k in dom (Decomp (n,2)) and A11: (Decomp (n,2)) . k = <*(k1 + 1),(n -' (k1 + 1))*> by FINSEQ_2:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; k1 + 0 < k1 + 1 by XREAL_1:6; then i < k by A1, A11, Th11; then i + 1 <= k by NAT_1:13; hence contradiction by A2, A5, A11, Th11; ::_thesis: verum end; theorem Th13: :: POLYNOM3:13 for n being Element of NAT holds (Decomp (n,2)) . 1 = <*0,n*> proof let n be Element of NAT ; ::_thesis: (Decomp (n,2)) . 1 = <*0,n*> consider A being finite Subset of (2 -tuples_on NAT) such that A1: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and A2: for p being Element of 2 -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; A3: now__::_thesis:_for_y_being_Element_of_2_-tuples_on_NAT_st_y_in_A_holds_ [<*0,n*>,y]_in_TuplesOrder_2 let y be Element of 2 -tuples_on NAT; ::_thesis: ( y in A implies [<*0,n*>,y] in TuplesOrder 2 ) consider d1, d2 being Element of NAT such that A4: y = <*d1,d2*> by FINSEQ_2:100; assume y in A ; ::_thesis: [<*0,n*>,y] in TuplesOrder 2 then Sum <*d1,d2*> = n by A2, A4; then A5: d1 + d2 = n by RVSUM_1:77; now__::_thesis:_<*0,n*>_<=_<*d1,d2*> percases ( d1 = 0 or d1 > 0 ) ; suppose d1 = 0 ; ::_thesis: <*0,n*> <= <*d1,d2*> hence <*0,n*> <= <*d1,d2*> by A5; ::_thesis: verum end; suppose d1 > 0 ; ::_thesis: <*0,n*> <= <*d1,d2*> then <*0,n*> . 1 < d1 by FINSEQ_1:44; then A6: <*0,n*> . 1 < <*d1,d2*> . 1 by FINSEQ_1:44; ( 1 in Seg 2 & ( for k being Element of NAT st 1 <= k & k < 1 holds <*0,n*> . k = <*d1,d2*> . k ) ) by FINSEQ_1:1; then <*0,n*> < <*d1,d2*> by A6, Def1; hence <*0,n*> <= <*d1,d2*> by Def2; ::_thesis: verum end; end; end; hence [<*0,n*>,y] in TuplesOrder 2 by A4, Def3; ::_thesis: verum end; 1 <= n + 1 by NAT_1:11; then 1 in Seg (n + 1) by FINSEQ_1:1; then 1 in Seg (len (Decomp (n,2))) by Th9; then A7: 1 in dom (Decomp (n,2)) by FINSEQ_1:def_3; field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15; then A8: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38; Sum <*0,n*> = 0 + n by RVSUM_1:77; then <*0,n*> in A by A2; then (SgmX ((TuplesOrder 2),A)) /. 1 = <*0,n*> by A8, A3, PRE_POLY:20; hence (Decomp (n,2)) . 1 = <*0,n*> by A1, A7, PARTFUN1:def_6; ::_thesis: verum end; theorem Th14: :: POLYNOM3:14 for n, i being Element of NAT st i in Seg (n + 1) holds (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> proof let n, i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> ) defpred S1[ Nat] means ( $1 <= n + 1 implies (Decomp (n,2)) . $1 = <*($1 -' 1),((n + 1) -' $1)*> ); assume i in Seg (n + 1) ; ::_thesis: (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> then A1: ( 1 <= i & i <= n + 1 ) by FINSEQ_1:1; consider A being finite Subset of (2 -tuples_on NAT) such that A2: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and A3: for p being Element of 2 -tuples_on NAT holds ( p in A iff Sum p = n ) by Def4; A4: for j being non empty Nat st S1[j] holds S1[j + 1] proof field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15; then A5: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38; let j be non empty Nat; ::_thesis: ( S1[j] implies S1[j + 1] ) assume that A6: ( j <= n + 1 implies (Decomp (n,2)) . j = <*(j -' 1),((n + 1) -' j)*> ) and A7: j + 1 <= n + 1 ; ::_thesis: (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*> n >= j by A7, XREAL_1:6; then A8: n - j >= 0 by XREAL_1:48; (n + 1) - (j + 1) >= 0 by A7, XREAL_1:48; then A9: (n + 1) -' (j + 1) = n - j by XREAL_0:def_2 .= n -' j by A8, XREAL_0:def_2 ; reconsider jj = j as non empty Element of NAT by ORDINAL1:def_12; j >= 1 by NAT_1:14; then A10: j - 1 >= 1 - 1 by XREAL_1:9; j + 1 >= 1 by NAT_1:11; then j + 1 in Seg (n + 1) by A7, FINSEQ_1:1; then j + 1 in Seg (len (Decomp (n,2))) by Th9; then A11: j + 1 in dom (Decomp (n,2)) by FINSEQ_1:def_3; then (Decomp (n,2)) . (j + 1) = (Decomp (n,2)) /. (j + 1) by PARTFUN1:def_6; then consider d1, d2 being Element of NAT such that A12: (Decomp (n,2)) . (j + 1) = <*d1,d2*> by FINSEQ_2:100; (Decomp (n,2)) . (j + 1) in rng (Decomp (n,2)) by A11, FUNCT_1:def_3; then (Decomp (n,2)) . (j + 1) in A by A2, A5, PRE_POLY:def_2; then Sum <*d1,d2*> = n by A3, A12; then A13: d1 + d2 = n by RVSUM_1:77; then n - d1 >= 0 ; then A14: d2 = n -' d1 by A13, XREAL_0:def_2; j < n + 1 by A7, NAT_1:13; then A15: (n + 1) - j >= 0 by XREAL_1:48; then n - (j - 1) >= 0 ; then A16: n - (j -' 1) >= 0 by A10, XREAL_0:def_2; (n + 1) -' j = n - (j - 1) by A15, XREAL_0:def_2 .= n - (j -' 1) by A10, XREAL_0:def_2 .= n -' (j -' 1) by A16, XREAL_0:def_2 ; then d1 = (jj -' 1) + 1 by A6, A7, A12, A14, Th12, NAT_1:13 .= j by NAT_1:14, XREAL_1:235 ; hence (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*> by A12, A14, A9, NAT_D:34; ::_thesis: verum end; A17: S1[1] proof assume 1 <= n + 1 ; ::_thesis: (Decomp (n,2)) . 1 = <*(1 -' 1),((n + 1) -' 1)*> thus (Decomp (n,2)) . 1 = <*0,n*> by Th13 .= <*(1 -' 1),n*> by XREAL_1:232 .= <*(1 -' 1),((n + 1) -' 1)*> by NAT_D:34 ; ::_thesis: verum end; for j being non empty Nat holds S1[j] from NAT_1:sch_10(A17, A4); hence (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> by A1; ::_thesis: verum end; definition let L be non empty multMagma ; let p, q, r be sequence of L; let t be FinSequence of 3 -tuples_on NAT; func prodTuples (p,q,r,t) -> Element of the carrier of L * means :Def5: :: POLYNOM3:def 5 ( len it = len t & ( for k being Element of NAT st k in dom t holds it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ); existence ex b1 being Element of the carrier of L * st ( len b1 = len t & ( for k being Element of NAT st k in dom t holds b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) proof deffunc H1( Nat) -> Element of the carrier of L = ((p . ((t /. $1) /. 1)) * (q . ((t /. $1) /. 2))) * (r . ((t /. $1) /. 3)); consider p1 being FinSequence of the carrier of L such that A1: len p1 = len t and A2: for k being Nat st k in dom p1 holds p1 . k = H1(k) from FINSEQ_2:sch_1(); A3: dom p1 = Seg (len t) by A1, FINSEQ_1:def_3; reconsider p1 = p1 as Element of the carrier of L * by FINSEQ_1:def_11; take p1 ; ::_thesis: ( len p1 = len t & ( for k being Element of NAT st k in dom t holds p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) thus len p1 = len t by A1; ::_thesis: for k being Element of NAT st k in dom t holds p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) let k be Element of NAT ; ::_thesis: ( k in dom t implies p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) assume k in dom t ; ::_thesis: p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) then k in Seg (len t) by FINSEQ_1:def_3; hence p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being Element of the carrier of L * st len b1 = len t & ( for k being Element of NAT st k in dom t holds b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len b2 = len t & ( for k being Element of NAT st k in dom t holds b2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) holds b1 = b2 proof let p1, p2 be Element of the carrier of L * ; ::_thesis: ( len p1 = len t & ( for k being Element of NAT st k in dom t holds p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len p2 = len t & ( for k being Element of NAT st k in dom t holds p2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) implies p1 = p2 ) assume that A4: len p1 = len t and A5: for k being Element of NAT st k in dom t holds p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) and A6: len p2 = len t and A7: for k being Element of NAT st k in dom t holds p2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ; ::_thesis: p1 = p2 A8: dom p1 = Seg (len t) by A4, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_p1_holds_ p1_._i_=_p2_._i let i be Nat; ::_thesis: ( i in dom p1 implies p1 . i = p2 . i ) assume i in dom p1 ; ::_thesis: p1 . i = p2 . i then A9: i in dom t by A8, FINSEQ_1:def_3; hence p1 . i = ((p . ((t /. i) /. 1)) * (q . ((t /. i) /. 2))) * (r . ((t /. i) /. 3)) by A5 .= p2 . i by A7, A9 ; ::_thesis: verum end; hence p1 = p2 by A4, A6, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def5 defines prodTuples POLYNOM3:def_5_:_ for L being non empty multMagma for p, q, r being sequence of L for t being FinSequence of 3 -tuples_on NAT for b6 being Element of the carrier of L * holds ( b6 = prodTuples (p,q,r,t) iff ( len b6 = len t & ( for k being Element of NAT st k in dom t holds b6 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) ); theorem Th15: :: POLYNOM3:15 for L being non empty multMagma for p, q, r being sequence of L for t being FinSequence of 3 -tuples_on NAT for P being Permutation of (dom t) for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P proof let L be non empty multMagma ; ::_thesis: for p, q, r being sequence of L for t being FinSequence of 3 -tuples_on NAT for P being Permutation of (dom t) for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P let p, q, r be sequence of L; ::_thesis: for t being FinSequence of 3 -tuples_on NAT for P being Permutation of (dom t) for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P let t be FinSequence of 3 -tuples_on NAT; ::_thesis: for P being Permutation of (dom t) for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P let P be Permutation of (dom t); ::_thesis: for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P let t1 be FinSequence of 3 -tuples_on NAT; ::_thesis: ( t1 = t * P implies prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P ) A1: rng P = dom t by FUNCT_2:def_3; assume A2: t1 = t * P ; ::_thesis: prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P then A3: dom P = dom t1 by A1, RELAT_1:27; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_t1_holds_ (prodTuples_(p,q,r,t1))_._x_=_((prodTuples_(p,q,r,t))_*_P)_._x let x be set ; ::_thesis: ( x in dom t1 implies (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x ) assume A5: x in dom t1 ; ::_thesis: (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x then reconsider i = x as Element of NAT ; A6: ( (prodTuples (p,q,r,t1)) . i = ((p . ((t1 /. i) /. 1)) * (q . ((t1 /. i) /. 2))) * (r . ((t1 /. i) /. 3)) & ((prodTuples (p,q,r,t)) * P) . x = (prodTuples (p,q,r,t)) . (P . x) ) by A3, A5, Def5, FUNCT_1:13; reconsider j = P . i as Element of NAT ; A7: P . i in rng P by A3, A5, FUNCT_1:def_3; t1 /. i = t1 . i by A5, PARTFUN1:def_6 .= t . (P . i) by A2, A5, FUNCT_1:12 .= t /. j by A1, A7, PARTFUN1:def_6 ; hence (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x by A1, A7, A6, Def5; ::_thesis: verum end; len (prodTuples (p,q,r,t1)) = len t1 by Def5; then A8: dom (prodTuples (p,q,r,t1)) = Seg (len t1) by FINSEQ_1:def_3; len (prodTuples (p,q,r,t)) = len t by Def5; then rng P = dom (prodTuples (p,q,r,t)) by A1, FINSEQ_3:29; then A9: dom ((prodTuples (p,q,r,t)) * P) = dom t1 by A3, RELAT_1:27; dom t1 = Seg (len t1) by FINSEQ_1:def_3; hence prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P by A8, A9, A4, FUNCT_1:2; ::_thesis: verum end; theorem Th16: :: POLYNOM3:16 for D being set for f being FinSequence of D * for i being Element of NAT holds Card (f | i) = (Card f) | i proof let D be set ; ::_thesis: for f being FinSequence of D * for i being Element of NAT holds Card (f | i) = (Card f) | i let f be FinSequence of D * ; ::_thesis: for i being Element of NAT holds Card (f | i) = (Card f) | i let i be Element of NAT ; ::_thesis: Card (f | i) = (Card f) | i A1: f | i = f | (Seg i) by FINSEQ_1:def_15; reconsider k = min (i,(len f)) as Element of NAT ; dom (Card (f | i)) = dom (f | i) by CARD_3:def_2; then A2: len (Card (f | i)) = len (f | i) by FINSEQ_3:29 .= min (i,(len f)) by A1, FINSEQ_2:21 ; then A3: dom (Card (f | i)) = Seg k by FINSEQ_1:def_3; A4: dom (Card f) = dom f by CARD_3:def_2; A5: (Card f) | i = (Card f) | (Seg i) by FINSEQ_1:def_15; A6: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_(f_|_i))_holds_ (Card_(f_|_i))_._j_=_((Card_f)_|_i)_._j A7: len f = len (Card f) by A4, FINSEQ_3:29; let j be Nat; ::_thesis: ( j in dom (Card (f | i)) implies (Card (f | i)) . b1 = ((Card f) | i) . b1 ) assume A8: j in dom (Card (f | i)) ; ::_thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1 percases ( i <= len f or i > len f ) ; supposeA9: i <= len f ; ::_thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1 A10: 1 <= j by A3, A8, FINSEQ_1:1; A11: k = i by A9, XXREAL_0:def_9; then j <= i by A3, A8, FINSEQ_1:1; then j <= len f by A9, XXREAL_0:2; then A12: j in dom f by A10, FINSEQ_3:25; len ((Card f) | i) = i by A7, A9, FINSEQ_1:59; then A13: dom ((Card f) | i) = Seg i by FINSEQ_1:def_3; reconsider Cf = Card f as FinSequence of NAT ; A14: Seg (len (f | i)) = dom (f | i) by FINSEQ_1:def_3; A15: len (f | i) = i by A9, FINSEQ_1:59; hence (Card (f | i)) . j = card ((f | i) . j) by A3, A8, A11, A14, CARD_3:def_2 .= card ((f | i) /. j) by A3, A8, A11, A15, A14, PARTFUN1:def_6 .= card (f /. j) by A3, A8, A11, A15, A14, FINSEQ_4:70 .= card (f . j) by A12, PARTFUN1:def_6 .= (Card f) . j by A12, CARD_3:def_2 .= Cf /. j by A4, A12, PARTFUN1:def_6 .= (Cf | i) /. j by A3, A8, A11, A13, FINSEQ_4:70 .= ((Card f) | i) . j by A3, A8, A11, A13, PARTFUN1:def_6 ; ::_thesis: verum end; supposeA16: i > len f ; ::_thesis: (Card (f | i)) . b1 = ((Card f) | i) . b1 then f | i = f by A1, FINSEQ_2:20; hence (Card (f | i)) . j = ((Card f) | i) . j by A5, A7, A16, FINSEQ_2:20; ::_thesis: verum end; end; end; len ((Card f) | i) = min (i,(len (Card f))) by A5, FINSEQ_2:21 .= min (i,(len f)) by A4, FINSEQ_3:29 ; hence Card (f | i) = (Card f) | i by A2, A6, FINSEQ_2:9; ::_thesis: verum end; theorem :: POLYNOM3:17 for p being FinSequence of REAL for q being FinSequence of NAT st p = q holds for i being Element of NAT holds p | i = q | i ; theorem Th18: :: POLYNOM3:18 for p being FinSequence of NAT for i, j being Element of NAT st i <= j holds Sum (p | i) <= Sum (p | j) proof let p be FinSequence of NAT ; ::_thesis: for i, j being Element of NAT st i <= j holds Sum (p | i) <= Sum (p | j) let i, j be Element of NAT ; ::_thesis: ( i <= j implies Sum (p | i) <= Sum (p | j) ) assume A1: i <= j ; ::_thesis: Sum (p | i) <= Sum (p | j) then consider k being Nat such that A2: j = i + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; percases ( j <= len p or j > len p ) ; supposeA3: j <= len p ; ::_thesis: Sum (p | i) <= Sum (p | j) then A4: len (p | j) = i + k by A2, FINSEQ_1:59; then consider q, r being FinSequence of NAT such that A5: len q = i and len r = k and A6: p | j = q ^ r by FINSEQ_2:23; A7: len (p | i) = i by A1, A3, FINSEQ_1:59, XXREAL_0:2; then A8: dom (p | i) = Seg i by FINSEQ_1:def_3; A9: now__::_thesis:_for_n_being_Nat_st_n_in_dom_(p_|_i)_holds_ (p_|_i)_._n_=_q_._n reconsider p1 = p as FinSequence of REAL ; let n be Nat; ::_thesis: ( n in dom (p | i) implies (p | i) . n = q . n ) assume A10: n in dom (p | i) ; ::_thesis: (p | i) . n = q . n then A11: (p1 | i) /. n = p /. n by FINSEQ_4:70; A12: Seg i = dom q by A5, FINSEQ_1:def_3; A13: ( Seg i c= Seg j & Seg j = dom (p | j) ) by A1, A2, A4, FINSEQ_1:5, FINSEQ_1:def_3; Seg i = dom (p | i) by A7, FINSEQ_1:def_3; then A14: (p1 | j) /. n = p /. n by A10, A13, FINSEQ_4:70; thus (p | i) . n = (p1 | i) /. n by A10, PARTFUN1:def_6 .= (p | j) . n by A8, A10, A13, A11, A14, PARTFUN1:def_6 .= q . n by A6, A8, A10, A12, FINSEQ_1:def_7 ; ::_thesis: verum end; A15: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6; Sum (p | j) = (Sum q) + (Sum r) by A6, RVSUM_1:75; hence Sum (p | i) <= Sum (p | j) by A7, A5, A9, A15, FINSEQ_2:9; ::_thesis: verum end; suppose j > len p ; ::_thesis: Sum (p | i) <= Sum (p | j) then A16: p | j = p by FINSEQ_1:58; now__::_thesis:_Sum_(p_|_i)_<=_Sum_(p_|_j) percases ( i >= len p or i < len p ) ; suppose i >= len p ; ::_thesis: Sum (p | i) <= Sum (p | j) hence Sum (p | i) <= Sum (p | j) by A16, FINSEQ_1:58; ::_thesis: verum end; supposeA17: i < len p ; ::_thesis: Sum (p | i) <= Sum (p | j) then consider t being Nat such that A18: len p = i + t by NAT_1:10; consider q, r being FinSequence of NAT such that A19: len q = i and len r = t and A20: p = q ^ r by A18, FINSEQ_2:23; A21: len (p | i) = i by A17, FINSEQ_1:59; then A22: dom (p | i) = Seg i by FINSEQ_1:def_3; A23: now__::_thesis:_for_n_being_Nat_st_n_in_dom_(p_|_i)_holds_ (p_|_i)_._n_=_q_._n A24: Seg i = dom q by A19, FINSEQ_1:def_3; reconsider p1 = p as FinSequence of REAL ; let n be Nat; ::_thesis: ( n in dom (p | i) implies (p | i) . n = q . n ) A25: dom (p | i) c= dom p by FINSEQ_5:18; assume A26: n in dom (p | i) ; ::_thesis: (p | i) . n = q . n then A27: (p1 | i) /. n = p /. n by FINSEQ_4:70; thus (p | i) . n = (p1 | i) /. n by A26, PARTFUN1:def_6 .= p . n by A26, A27, A25, PARTFUN1:def_6 .= q . n by A20, A22, A26, A24, FINSEQ_1:def_7 ; ::_thesis: verum end; A28: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6; Sum p = (Sum q) + (Sum r) by A20, RVSUM_1:75; hence Sum (p | i) <= Sum (p | j) by A16, A19, A21, A23, A28, FINSEQ_2:9; ::_thesis: verum end; end; end; hence Sum (p | i) <= Sum (p | j) ; ::_thesis: verum end; end; end; theorem :: POLYNOM3:19 for D being set for p being FinSequence of D for i being Element of NAT st i < len p holds p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by FINSEQ_5:83; theorem Th20: :: POLYNOM3:20 for p being FinSequence of REAL for i being Element of NAT st i < len p holds Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) proof let p be FinSequence of REAL ; ::_thesis: for i being Element of NAT st i < len p holds Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) let i be Element of NAT ; ::_thesis: ( i < len p implies Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) ) assume i < len p ; ::_thesis: Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) then p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by FINSEQ_5:83; hence Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) by RVSUM_1:74; ::_thesis: verum end; theorem Th21: :: POLYNOM3:21 for p being FinSequence of NAT for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds ( i = j & k1 = k2 ) proof let p be FinSequence of NAT ; ::_thesis: for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds ( i = j & k1 = k2 ) let i, j, k1, k2 be Element of NAT ; ::_thesis: ( i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 implies ( i = j & k1 = k2 ) ) assume that A1: i < len p and A2: j < len p and A3: 1 <= k1 and A4: 1 <= k2 and A5: k1 <= p . (i + 1) and A6: k2 <= p . (j + 1) and A7: (Sum (p | i)) + k1 = (Sum (p | j)) + k2 and A8: ( i <> j or k1 <> k2 ) ; ::_thesis: contradiction A9: i <> j by A7, A8, XCMPLX_1:2; reconsider p1 = p as FinSequence of REAL ; A10: (Sum (p1 | i)) + (p . (i + 1)) >= (Sum (p | i)) + k1 by A5, XREAL_1:6; A11: (Sum (p1 | j)) + (p . (j + 1)) >= (Sum (p | j)) + k2 by A6, XREAL_1:6; percases ( i < j or i >= j ) ; suppose i < j ; ::_thesis: contradiction then i + 1 <= j by NAT_1:13; then Sum (p | j) >= Sum (p1 | (i + 1)) by Th18; then Sum (p | j) >= (Sum (p1 | i)) + (p . (i + 1)) by A1, Th20; then A12: Sum (p | j) >= (Sum (p | j)) + k2 by A7, A10, XXREAL_0:2; (Sum (p | j)) + k2 >= Sum (p | j) by NAT_1:11; then Sum (p | j) = (Sum (p | j)) + k2 by A12, XXREAL_0:1; then k2 = 0 ; hence contradiction by A4; ::_thesis: verum end; suppose i >= j ; ::_thesis: contradiction then j < i by A9, XXREAL_0:1; then j + 1 <= i by NAT_1:13; then Sum (p | i) >= Sum (p1 | (j + 1)) by Th18; then Sum (p | i) >= (Sum (p1 | j)) + (p . (j + 1)) by A2, Th20; then A13: Sum (p | i) >= (Sum (p | i)) + k1 by A7, A11, XXREAL_0:2; (Sum (p | i)) + k1 >= Sum (p | i) by NAT_1:11; then Sum (p | i) = (Sum (p | i)) + k1 by A13, XXREAL_0:1; then k1 = 0 ; hence contradiction by A3; ::_thesis: verum end; end; end; theorem Th22: :: POLYNOM3:22 for D1, D2 being set for f1 being FinSequence of D1 * for f2 being FinSequence of D2 * for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds ( i1 = i2 & j1 = j2 ) proof let D1, D2 be set ; ::_thesis: for f1 being FinSequence of D1 * for f2 being FinSequence of D2 * for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds ( i1 = i2 & j1 = j2 ) let f1 be FinSequence of D1 * ; ::_thesis: for f2 being FinSequence of D2 * for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds ( i1 = i2 & j1 = j2 ) let f2 be FinSequence of D2 * ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds ( i1 = i2 & j1 = j2 ) let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 implies ( i1 = i2 & j1 = j2 ) ) assume that A1: i1 in dom f1 and A2: i2 in dom f2 and A3: j1 in dom (f1 . i1) and A4: j2 in dom (f2 . i2) and A5: ( Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 ) ; ::_thesis: ( i1 = i2 & j1 = j2 ) A6: ( j1 >= 1 & j2 >= 1 ) by A3, A4, FINSEQ_3:25; A7: 1 <= i1 by A1, FINSEQ_3:25; then A8: i1 - 1 >= 0 by XREAL_1:48; j1 <= len (f1 . i1) by A3, FINSEQ_3:25; then j1 <= (Card f1) . i1 by A1, CARD_3:def_2; then A9: j1 <= (Card f1) . ((i1 -' 1) + 1) by A7, XREAL_1:235; A10: 1 <= i2 by A2, FINSEQ_3:25; then A11: i2 - 1 >= 0 by XREAL_1:48; dom (Card f2) = dom f2 by CARD_3:def_2; then A12: len (Card f2) = len f2 by FINSEQ_3:29; dom (Card f1) = dom f1 by CARD_3:def_2; then A13: len (Card f1) = len f1 by FINSEQ_3:29; i1 <= len f1 by A1, FINSEQ_3:25; then i1 < (len f1) + 1 by NAT_1:13; then i1 - 1 < ((len f1) + 1) - 1 by XREAL_1:9; then A14: i1 -' 1 < len (Card f1) by A13, A8, XREAL_0:def_2; j2 <= len (f2 . i2) by A4, FINSEQ_3:25; then j2 <= (Card f2) . i2 by A2, CARD_3:def_2; then A15: j2 <= (Card f2) . ((i2 -' 1) + 1) by A10, XREAL_1:235; i2 <= len f2 by A2, FINSEQ_3:25; then i2 < (len f2) + 1 by NAT_1:13; then i2 - 1 < ((len f2) + 1) - 1 by XREAL_1:9; then i2 -' 1 < len (Card f2) by A12, A11, XREAL_0:def_2; then i1 -' 1 = i2 -' 1 by A5, A14, A6, A9, A15, Th21; then i1 - 1 = i2 -' 1 by A8, XREAL_0:def_2; then i1 - 1 = i2 - 1 by A11, XREAL_0:def_2; hence ( i1 = i2 & j1 = j2 ) by A5, A14, A6, A9, A15, Th21; ::_thesis: verum end; begin definition let L be non empty ZeroStr ; mode Polynomial of L is AlgSequence of L; end; theorem Th23: :: POLYNOM3:23 for L being non empty ZeroStr for p being Polynomial of L for n being Element of NAT holds ( n >= len p iff n is_at_least_length_of p ) proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L for n being Element of NAT holds ( n >= len p iff n is_at_least_length_of p ) let p be Polynomial of L; ::_thesis: for n being Element of NAT holds ( n >= len p iff n is_at_least_length_of p ) let n be Element of NAT ; ::_thesis: ( n >= len p iff n is_at_least_length_of p ) thus ( n >= len p implies n is_at_least_length_of p ) ::_thesis: ( n is_at_least_length_of p implies n >= len p ) proof assume A1: n >= len p ; ::_thesis: n is_at_least_length_of p let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not n <= i or p . i = 0. L ) assume i >= n ; ::_thesis: p . i = 0. L hence p . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2; ::_thesis: verum end; assume n is_at_least_length_of p ; ::_thesis: n >= len p hence n >= len p by ALGSEQ_1:def_3; ::_thesis: verum end; scheme :: POLYNOM3:sch 2 PolynomialLambdaF{ F1() -> non empty addLoopStr , F2() -> Element of NAT , F3( Element of NAT ) -> Element of F1() } : ex p being Polynomial of F1() st ( len p <= F2() & ( for n being Element of NAT st n < F2() holds p . n = F3(n) ) ) proof defpred S1[ Element of NAT , Element of F1()] means ( ( $1 < F2() & $2 = F3($1) ) or ( $1 >= F2() & $2 = 0. F1() ) ); A1: for x being Element of NAT ex y being Element of F1() st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of F1() st S1[x,y] ( x < F2() implies ( x < F2() & F3(x) = F3(x) ) ) ; hence ex y being Element of F1() st S1[x,y] ; ::_thesis: verum end; ex f being Function of NAT, the carrier of F1() st for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1); then consider f being Function of NAT, the carrier of F1() such that A2: for x being Element of NAT holds ( ( x < F2() & f . x = F3(x) ) or ( x >= F2() & f . x = 0. F1() ) ) ; ex n being Nat st for i being Nat st i >= n holds f . i = 0. F1() proof take F2() ; ::_thesis: for i being Nat st i >= F2() holds f . i = 0. F1() let i be Nat; ::_thesis: ( i >= F2() implies f . i = 0. F1() ) i in NAT by ORDINAL1:def_12; hence ( i >= F2() implies f . i = 0. F1() ) by A2; ::_thesis: verum end; then reconsider f = f as AlgSequence of F1() by ALGSEQ_1:def_1; take f ; ::_thesis: ( len f <= F2() & ( for n being Element of NAT st n < F2() holds f . n = F3(n) ) ) now__::_thesis:_for_i_being_Nat_st_i_>=_F2()_holds_ f_._i_=_0._F1() let i be Nat; ::_thesis: ( i >= F2() implies f . i = 0. F1() ) i in NAT by ORDINAL1:def_12; hence ( i >= F2() implies f . i = 0. F1() ) by A2; ::_thesis: verum end; then F2() is_at_least_length_of f by ALGSEQ_1:def_2; hence ( len f <= F2() & ( for n being Element of NAT st n < F2() holds f . n = F3(n) ) ) by A2, ALGSEQ_1:def_3; ::_thesis: verum end; registration let L be non empty right_zeroed addLoopStr ; let p, q be Polynomial of L; clusterp + q -> finite-Support ; coherence p + q is finite-Support proof take s = (len p) + (len q); :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds ( not s <= b1 or (p + q) . b1 = 0. L ) let i be Nat; ::_thesis: ( not s <= i or (p + q) . i = 0. L ) assume A1: i >= s ; ::_thesis: (p + q) . i = 0. L (len p) + (len q) >= len p by NAT_1:11; then A2: p . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2; A3: (len p) + (len q) >= len q by NAT_1:11; i in NAT by ORDINAL1:def_12; hence (p + q) . i = (p . i) + (q . i) by NORMSP_1:def_2 .= (0. L) + (0. L) by A1, A2, A3, ALGSEQ_1:8, XXREAL_0:2 .= 0. L by RLVECT_1:def_4 ; ::_thesis: verum end; end; theorem Th24: :: POLYNOM3:24 for L being non empty right_zeroed addLoopStr for p, q being Polynomial of L for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds n is_at_least_length_of p + q proof let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of L for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds n is_at_least_length_of p + q let p, q be Polynomial of L; ::_thesis: for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds n is_at_least_length_of p + q let n be Element of NAT ; ::_thesis: ( n is_at_least_length_of p & n is_at_least_length_of q implies n is_at_least_length_of p + q ) assume A1: ( n is_at_least_length_of p & n is_at_least_length_of q ) ; ::_thesis: n is_at_least_length_of p + q let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not n <= i or (p + q) . i = 0. L ) assume i >= n ; ::_thesis: (p + q) . i = 0. L then A2: ( p . i = 0. L & q . i = 0. L ) by A1, ALGSEQ_1:def_2; i in NAT by ORDINAL1:def_12; hence (p + q) . i = (0. L) + (0. L) by A2, NORMSP_1:def_2 .= 0. L by RLVECT_1:def_4 ; ::_thesis: verum end; theorem :: POLYNOM3:25 for L being non empty right_zeroed addLoopStr for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q) proof let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q) let p, q be Polynomial of L; ::_thesis: support (p + q) c= (support p) \/ (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 x1 = x as Element of NAT ; A2: x1 < len (p + q) by A1, ALGSEQ_1:1; ( x1 < len p or x1 < len q ) proof assume ( not x1 < len p & not x1 < len q ) ; ::_thesis: contradiction then ( x1 is_at_least_length_of p & x1 is_at_least_length_of q ) by Th23; then x1 is_at_least_length_of p + q by Th24; hence contradiction by A2, Th23; ::_thesis: verum end; then ( x in Segm (len p) or x in Segm (len q) ) by NAT_1:44; hence x in (support p) \/ (support q) by XBOOLE_0:def_3; ::_thesis: verum end; definition let L be non empty Abelian addLoopStr ; let p, q be sequence of L; :: original: + redefine funcp + q -> Element of bool [:NAT, the carrier of L:]; commutativity for p, q being sequence of L holds p + q = q + p proof let p, q be sequence of L; ::_thesis: p + q = q + p now__::_thesis:_for_n_being_Element_of_NAT_holds_(p_+_q)_._n_=_(q_+_p)_._n let n be Element of NAT ; ::_thesis: (p + q) . n = (q + p) . n thus (p + q) . n = (p . n) + (q . n) by NORMSP_1:def_2 .= (q + p) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence p + q = q + p by FUNCT_2:63; ::_thesis: verum end; end; theorem Th26: :: POLYNOM3:26 for L being non empty add-associative addLoopStr for p, q, r being sequence of L holds (p + q) + r = p + (q + r) proof let L be non empty add-associative addLoopStr ; ::_thesis: for p, q, r being sequence of L holds (p + q) + r = p + (q + r) let p, q, r be sequence of L; ::_thesis: (p + q) + r = p + (q + r) now__::_thesis:_for_n_being_Element_of_NAT_holds_((p_+_q)_+_r)_._n_=_(p_+_(q_+_r))_._n let n be Element of NAT ; ::_thesis: ((p + q) + r) . n = (p + (q + r)) . n thus ((p + q) + r) . n = ((p + q) . n) + (r . n) by NORMSP_1:def_2 .= ((p . n) + (q . n)) + (r . n) by NORMSP_1:def_2 .= (p . n) + ((q . n) + (r . n)) by RLVECT_1:def_3 .= (p . n) + ((q + r) . n) by NORMSP_1:def_2 .= (p + (q + r)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence (p + q) + r = p + (q + r) by FUNCT_2:63; ::_thesis: verum end; registration let L be non empty right_complementable add-associative right_zeroed addLoopStr ; let p be Polynomial of L; cluster - p -> finite-Support ; coherence - p is finite-Support proof take s = len p; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds ( not s <= b1 or (- p) . b1 = 0. L ) let i be Nat; ::_thesis: ( not s <= i or (- p) . i = 0. L ) assume A1: i >= s ; ::_thesis: (- p) . i = 0. L i in NAT by ORDINAL1:def_12; hence (- p) . i = - (p . i) by BHSP_1:44 .= - (0. L) by A1, ALGSEQ_1:8 .= 0. L by RLVECT_1:12 ; ::_thesis: verum end; end; Lm1: for L being non empty addLoopStr for p, q being sequence of L holds p - q = p + (- q) proof let L be non empty addLoopStr ; ::_thesis: for p, q being sequence of L holds p - q = p + (- q) let p, q be sequence of L; ::_thesis: p - q = p + (- q) let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (p - q) . n = (p + (- q)) . n thus (p - q) . n = (p . n) - (q . n) by NORMSP_1:def_3 .= (p . n) + ((- q) . n) by BHSP_1:44 .= (p + (- q)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; definition let L be non empty addLoopStr ; let p, q be sequence of L; redefine func p - q equals :: POLYNOM3:def 6 p + (- q); compatibility for b1 being Element of bool [:NAT, the carrier of L:] holds ( b1 = p - q iff b1 = p + (- q) ) by Lm1; end; :: deftheorem defines - POLYNOM3:def_6_:_ for L being non empty addLoopStr for p, q being sequence of L holds p - q = p + (- q); registration let L be non empty right_complementable add-associative right_zeroed addLoopStr ; let p, q be Polynomial of L; clusterp - q -> finite-Support ; coherence p - q is finite-Support ; end; theorem :: POLYNOM3:27 for L being non empty addLoopStr for p, q being sequence of L for n being Element of NAT holds (p - q) . n = (p . n) - (q . n) by NORMSP_1:def_3; definition let L be non empty ZeroStr ; func 0_. L -> sequence of L equals :: POLYNOM3:def 7 NAT --> (0. L); coherence NAT --> (0. L) is sequence of L ; end; :: deftheorem defines 0_. POLYNOM3:def_7_:_ for L being non empty ZeroStr holds 0_. L = NAT --> (0. L); registration let L be non empty ZeroStr ; cluster 0_. L -> finite-Support ; coherence 0_. L is finite-Support proof take 0 ; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds ( not 0 <= b1 or (0_. L) . b1 = 0. L ) let i be Nat; ::_thesis: ( not 0 <= i or (0_. L) . i = 0. L ) assume i >= 0 ; ::_thesis: (0_. L) . i = 0. L i in NAT by ORDINAL1:def_12; hence (0_. L) . i = 0. L by FUNCOP_1:7; ::_thesis: verum end; end; theorem Th28: :: POLYNOM3:28 for L being non empty right_zeroed addLoopStr for p being sequence of L holds p + (0_. L) = p proof let L be non empty right_zeroed addLoopStr ; ::_thesis: for p being sequence of L holds p + (0_. L) = p let p be sequence of L; ::_thesis: p + (0_. L) = p now__::_thesis:_for_n_being_Element_of_NAT_holds_(p_+_(0_._L))_._n_=_p_._n let n be Element of NAT ; ::_thesis: (p + (0_. L)) . n = p . n thus (p + (0_. L)) . n = (p . n) + ((0_. L) . n) by NORMSP_1:def_2 .= (p . n) + (0. L) by FUNCOP_1:7 .= p . n by RLVECT_1:def_4 ; ::_thesis: verum end; hence p + (0_. L) = p by FUNCT_2:63; ::_thesis: verum end; theorem Th29: :: POLYNOM3:29 for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being sequence of L holds p - p = 0_. L proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being sequence of L holds p - p = 0_. L let p be sequence of L; ::_thesis: p - p = 0_. L now__::_thesis:_for_n_being_Element_of_NAT_holds_(p_-_p)_._n_=_(0_._L)_._n let n be Element of NAT ; ::_thesis: (p - p) . n = (0_. L) . n thus (p - p) . n = (p . n) - (p . n) by NORMSP_1:def_3 .= 0. L by RLVECT_1:15 .= (0_. L) . n by FUNCOP_1:7 ; ::_thesis: verum end; hence p - p = 0_. L by FUNCT_2:63; ::_thesis: verum end; definition let L be non empty multLoopStr_0 ; func 1_. L -> sequence of L equals :: POLYNOM3:def 8 (0_. L) +* (0,(1. L)); coherence (0_. L) +* (0,(1. L)) is sequence of L ; end; :: deftheorem defines 1_. POLYNOM3:def_8_:_ for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L)); registration let L be non empty multLoopStr_0 ; cluster 1_. L -> finite-Support ; coherence 1_. L is finite-Support proof take 1 ; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds ( not 1 <= b1 or (1_. L) . b1 = 0. L ) let i be Nat; ::_thesis: ( not 1 <= i or (1_. L) . i = 0. L ) A1: i in NAT by ORDINAL1:def_12; assume i >= 1 ; ::_thesis: (1_. L) . i = 0. L hence (1_. L) . i = (0_. L) . i by FUNCT_7:32 .= 0. L by A1, FUNCOP_1:7 ; ::_thesis: verum end; end; theorem Th30: :: POLYNOM3:30 for L being non empty multLoopStr_0 holds ( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds (1_. L) . n = 0. L ) ) proof let L be non empty multLoopStr_0 ; ::_thesis: ( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds (1_. L) . n = 0. L ) ) 0 in NAT ; then 0 in dom (0_. L) by FUNCT_2:def_1; hence (1_. L) . 0 = 1. L by FUNCT_7:31; ::_thesis: for n being Nat st n <> 0 holds (1_. L) . n = 0. L let n be Nat; ::_thesis: ( n <> 0 implies (1_. L) . n = 0. L ) A1: n in NAT by ORDINAL1:def_12; assume n <> 0 ; ::_thesis: (1_. L) . n = 0. L hence (1_. L) . n = (0_. L) . n by FUNCT_7:32 .= 0. L by A1, FUNCOP_1:7 ; ::_thesis: verum end; definition let L be non empty doubleLoopStr ; let p, q be sequence of L; funcp *' q -> sequence of L means :Def9: :: POLYNOM3:def 9 for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & it . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ); existence ex b1 being sequence of L st for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & b1 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) proof defpred S1[ Element of NAT , Element of L] means ex r being FinSequence of the carrier of L st ( len r = $1 + 1 & $2 = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . (($1 + 1) -' k)) ) ); A1: for i being Element of NAT ex v being Element of L st S1[i,v] proof let i be Element of NAT ; ::_thesis: ex v being Element of L st S1[i,v] deffunc H1( Nat) -> Element of the carrier of L = (p . ($1 -' 1)) * (q . ((i + 1) -' $1)); consider r being FinSequence of the carrier of L such that A2: len r = i + 1 and A3: for k being Nat st k in dom r holds r . k = H1(k) from FINSEQ_2:sch_1(); take v = Sum r; ::_thesis: S1[i,v] take r ; ::_thesis: ( len r = i + 1 & v = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) thus len r = i + 1 by A2; ::_thesis: ( v = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) thus v = Sum r ; ::_thesis: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) let k be Element of NAT ; ::_thesis: ( k in dom r implies r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) assume k in dom r ; ::_thesis: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) hence r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3; ::_thesis: verum end; consider f being Function of NAT, the carrier of L such that A4: for i being Element of NAT holds S1[i,f . i] from FUNCT_2:sch_3(A1); take f ; ::_thesis: for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & f . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) thus for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & f . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) by A4; ::_thesis: verum end; uniqueness for b1, b2 being sequence of L st ( for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & b1 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & b2 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds b1 = b2 proof let p1, p2 be sequence of L; ::_thesis: ( ( for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & p1 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & p2 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) implies p1 = p2 ) assume that A5: for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & p1 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) and A6: for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & p2 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ; ::_thesis: p1 = p2 now__::_thesis:_for_i_being_Element_of_NAT_holds_p1_._i_=_p2_._i let i be Element of NAT ; ::_thesis: p1 . i = p2 . i consider r1 being FinSequence of the carrier of L such that A7: len r1 = i + 1 and A8: p1 . i = Sum r1 and A9: for k being Element of NAT st k in dom r1 holds r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A5; consider r2 being FinSequence of the carrier of L such that A10: len r2 = i + 1 and A11: p2 . i = Sum r2 and A12: for k being Element of NAT st k in dom r2 holds r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A6; A13: dom r1 = Seg (len r2) by A7, A10, FINSEQ_1:def_3 .= dom r2 by FINSEQ_1:def_3 ; now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_ r1_._k_=_r2_._k let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = r2 . k ) assume A14: k in dom r1 ; ::_thesis: r1 . k = r2 . k hence r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A9 .= r2 . k by A12, A13, A14 ; ::_thesis: verum end; hence p1 . i = p2 . i by A8, A11, A13, FINSEQ_1:13; ::_thesis: verum end; hence p1 = p2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def9 defines *' POLYNOM3:def_9_:_ for L being non empty doubleLoopStr for p, q, b4 being sequence of L holds ( b4 = p *' q iff for i being Element of NAT ex r being FinSequence of the carrier of L st ( len r = i + 1 & b4 . i = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ); registration let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; let p, q be Polynomial of L; clusterp *' q -> finite-Support ; coherence p *' q is finite-Support proof take s = (len p) + (len q); :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds ( not s <= b1 or (p *' q) . b1 = 0. L ) let i be Nat; ::_thesis: ( not s <= i or (p *' q) . i = 0. L ) i in NAT by ORDINAL1:def_12; then consider r being FinSequence of the carrier of L such that A1: len r = i + 1 and A2: (p *' q) . i = Sum r and A3: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9; assume i >= s ; ::_thesis: (p *' q) . i = 0. L then len p <= i - (len q) by XREAL_1:19; then A4: - (len p) >= - (i - (len q)) by XREAL_1:24; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r implies r . b1 = 0. L ) assume A5: k in dom r ; ::_thesis: r . b1 = 0. L then A6: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3; k <= i + 1 by A1, A5, FINSEQ_3:25; then A7: (i + 1) - k >= 0 by XREAL_1:48; percases ( k -' 1 < len p or k -' 1 >= len p ) ; suppose k -' 1 < len p ; ::_thesis: r . b1 = 0. L then k - 1 < len p by XREAL_0:def_2; then - (k - 1) > - (len p) by XREAL_1:24; then 1 - k > (len q) - i by A4, XXREAL_0:2; then i + (1 - k) > len q by XREAL_1:19; then (i + 1) -' k >= len q by A7, XREAL_0:def_2; then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8; hence r . k = 0. L by A6, VECTSP_1:6; ::_thesis: verum end; suppose k -' 1 >= len p ; ::_thesis: r . b1 = 0. L then p . (k -' 1) = 0. L by ALGSEQ_1:8; hence r . k = 0. L by A6, VECTSP_1:7; ::_thesis: verum end; end; end; hence (p *' q) . i = 0. L by A2, Th1; ::_thesis: verum end; end; theorem Th31: :: POLYNOM3:31 for L being non empty right_complementable right-distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r) proof let L be non empty right_complementable right-distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r) let p, q, r be sequence of L; ::_thesis: p *' (q + r) = (p *' q) + (p *' r) now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(q_+_r))_._i_=_((p_*'_q)_+_(p_*'_r))_._i let i be Element of NAT ; ::_thesis: (p *' (q + r)) . i = ((p *' q) + (p *' r)) . i consider r1 being FinSequence of the carrier of L such that A1: len r1 = i + 1 and A2: (p *' (q + r)) . i = Sum r1 and A3: for k being Element of NAT st k in dom r1 holds r1 . k = (p . (k -' 1)) * ((q + r) . ((i + 1) -' k)) by Def9; A4: dom r1 = Seg (i + 1) by A1, FINSEQ_1:def_3; consider r3 being FinSequence of the carrier of L such that A5: len r3 = i + 1 and A6: (p *' r) . i = Sum r3 and A7: for k being Element of NAT st k in dom r3 holds r3 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by Def9; consider r2 being FinSequence of the carrier of L such that A8: len r2 = i + 1 and A9: (p *' q) . i = Sum r2 and A10: for k being Element of NAT st k in dom r2 holds r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9; reconsider r29 = r2, r39 = r3 as Element of (i + 1) -tuples_on the carrier of L by A8, A5, FINSEQ_2:92; A11: len (r29 + r39) = i + 1 by CARD_1:def_7; now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_ r1_._k_=_(r2_+_r3)_._k let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = (r2 + r3) . k ) assume A12: k in dom r1 ; ::_thesis: r1 . k = (r2 + r3) . k then A13: k in dom (r2 + r3) by A11, A4, FINSEQ_1:def_3; k in dom r3 by A5, A4, A12, FINSEQ_1:def_3; then A14: r3 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by A7; k in dom r2 by A8, A4, A12, FINSEQ_1:def_3; then A15: r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A10; thus r1 . k = (p . (k -' 1)) * ((q + r) . ((i + 1) -' k)) by A3, A12 .= (p . (k -' 1)) * ((q . ((i + 1) -' k)) + (r . ((i + 1) -' k))) by NORMSP_1:def_2 .= ((p . (k -' 1)) * (q . ((i + 1) -' k))) + ((p . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def_2 .= (r2 + r3) . k by A13, A15, A14, FVSUM_1:17 ; ::_thesis: verum end; then Sum r1 = Sum (r29 + r39) by A1, A11, FINSEQ_2:9 .= (Sum r2) + (Sum r3) by FVSUM_1:76 ; hence (p *' (q + r)) . i = ((p *' q) + (p *' r)) . i by A2, A9, A6, NORMSP_1:def_2; ::_thesis: verum end; hence p *' (q + r) = (p *' q) + (p *' r) by FUNCT_2:63; ::_thesis: verum end; theorem Th32: :: POLYNOM3:32 for L being non empty right_complementable left-distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r) proof let L be non empty right_complementable left-distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r) let p, q, r be sequence of L; ::_thesis: (p + q) *' r = (p *' r) + (q *' r) now__::_thesis:_for_i_being_Element_of_NAT_holds_((p_+_q)_*'_r)_._i_=_((p_*'_r)_+_(q_*'_r))_._i let i be Element of NAT ; ::_thesis: ((p + q) *' r) . i = ((p *' r) + (q *' r)) . i consider r1 being FinSequence of the carrier of L such that A1: len r1 = i + 1 and A2: ((p + q) *' r) . i = Sum r1 and A3: for k being Element of NAT st k in dom r1 holds r1 . k = ((p + q) . (k -' 1)) * (r . ((i + 1) -' k)) by Def9; A4: dom r1 = Seg (i + 1) by A1, FINSEQ_1:def_3; consider r3 being FinSequence of the carrier of L such that A5: len r3 = i + 1 and A6: (q *' r) . i = Sum r3 and A7: for k being Element of NAT st k in dom r3 holds r3 . k = (q . (k -' 1)) * (r . ((i + 1) -' k)) by Def9; consider r2 being FinSequence of the carrier of L such that A8: len r2 = i + 1 and A9: (p *' r) . i = Sum r2 and A10: for k being Element of NAT st k in dom r2 holds r2 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by Def9; reconsider r29 = r2, r39 = r3 as Element of (i + 1) -tuples_on the carrier of L by A8, A5, FINSEQ_2:92; A11: len (r29 + r39) = i + 1 by CARD_1:def_7; now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_ r1_._k_=_(r2_+_r3)_._k let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = (r2 + r3) . k ) assume A12: k in dom r1 ; ::_thesis: r1 . k = (r2 + r3) . k then A13: k in dom (r2 + r3) by A11, A4, FINSEQ_1:def_3; k in dom r3 by A5, A4, A12, FINSEQ_1:def_3; then A14: r3 . k = (q . (k -' 1)) * (r . ((i + 1) -' k)) by A7; k in dom r2 by A8, A4, A12, FINSEQ_1:def_3; then A15: r2 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by A10; thus r1 . k = ((p + q) . (k -' 1)) * (r . ((i + 1) -' k)) by A3, A12 .= ((p . (k -' 1)) + (q . (k -' 1))) * (r . ((i + 1) -' k)) by NORMSP_1:def_2 .= ((p . (k -' 1)) * (r . ((i + 1) -' k))) + ((q . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def_3 .= (r2 + r3) . k by A13, A15, A14, FVSUM_1:17 ; ::_thesis: verum end; then Sum r1 = Sum (r29 + r39) by A1, A11, FINSEQ_2:9 .= (Sum r2) + (Sum r3) by FVSUM_1:76 ; hence ((p + q) *' r) . i = ((p *' r) + (q *' r)) . i by A2, A9, A6, NORMSP_1:def_2; ::_thesis: verum end; hence (p + q) *' r = (p *' r) + (q *' r) by FUNCT_2:63; ::_thesis: verum end; definition let n be Element of NAT ; :: original: <* redefine func<*n*> -> Element of 1 -tuples_on NAT; coherence <*n*> is Element of 1 -tuples_on NAT proof thus <*n*> is Element of 1 -tuples_on NAT by FINSEQ_2:131; ::_thesis: verum end; end; theorem Th33: :: POLYNOM3:33 for L being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r) proof let L be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r) let p, q, r be sequence of L; ::_thesis: (p *' q) *' r = p *' (q *' r) now__::_thesis:_for_i_being_Element_of_NAT_holds_((p_*'_q)_*'_r)_._i_=_(p_*'_(q_*'_r))_._i let i be Element of NAT ; ::_thesis: ((p *' q) *' r) . i = (p *' (q *' r)) . i deffunc H1( Nat) -> Element of ((2 + 1) -tuples_on NAT) * = (Decomp (($1 -' 1),2)) ^^ ($1 |-> <*((i + 1) -' $1)*>); consider f2 being FinSequence of ((2 + 1) -tuples_on NAT) * such that A1: len f2 = i + 1 and A2: for k being Nat st k in dom f2 holds f2 . k = H1(k) from FINSEQ_2:sch_1(); A3: dom f2 = Seg (i + 1) by A1, FINSEQ_1:def_3; reconsider f2 = f2 as FinSequence of (3 -tuples_on NAT) * ; deffunc H2( Nat) -> Element of ((1 + 2) -tuples_on NAT) * = (((i + 2) -' $1) |-> <*($1 -' 1)*>) ^^ (Decomp (((i + 1) -' $1),2)); consider g2 being FinSequence of ((1 + 2) -tuples_on NAT) * such that A4: len g2 = i + 1 and A5: for k being Nat st k in dom g2 holds g2 . k = H2(k) from FINSEQ_2:sch_1(); A6: dom g2 = Seg (i + 1) by A4, FINSEQ_1:def_3; reconsider g2 = g2 as FinSequence of (3 -tuples_on NAT) * ; consider r2 being FinSequence of the carrier of L such that A7: len r2 = i + 1 and A8: (p *' (q *' r)) . i = Sum r2 and A9: for k being Element of NAT st k in dom r2 holds r2 . k = (p . (k -' 1)) * ((q *' r) . ((i + 1) -' k)) by Def9; A10: dom r2 = Seg (i + 1) by A7, FINSEQ_1:def_3; A11: dom (Card f2) = dom f2 by CARD_3:def_2 .= Seg (len g2) by A1, A4, FINSEQ_1:def_3 .= dom g2 by FINSEQ_1:def_3 .= dom (Card g2) by CARD_3:def_2 .= dom (Rev (Card g2)) by FINSEQ_5:57 ; A12: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_f2)_holds_ (Card_f2)_._j_=_(Rev_(Card_g2))_._j let j be Nat; ::_thesis: ( j in dom (Card f2) implies (Card f2) . j = (Rev (Card g2)) . j ) A13: dom (j |-> <*((i + 1) -' j)*>) = Seg j by FUNCOP_1:13; assume A14: j in dom (Card f2) ; ::_thesis: (Card f2) . j = (Rev (Card g2)) . j then A15: j in Seg (len (Rev (Card g2))) by A11, FINSEQ_1:def_3; then A16: j >= 1 by FINSEQ_1:1; then j - 1 >= 0 by XREAL_1:48; then A17: (i + 1) - (j - 1) <= i + 1 by XREAL_1:43; A18: dom (Card g2) = dom g2 by CARD_3:def_2; then A19: len (Card g2) = len g2 by FINSEQ_3:29; then A20: j in Seg (len g2) by A15, FINSEQ_5:def_3; then A21: f2 . j = (Decomp ((j -' 1),2)) ^^ (j |-> <*((i + 1) -' j)*>) by A2, A3, A4; i + 1 >= j by A4, A20, FINSEQ_1:1; then A22: (i + 1) - j >= 0 by XREAL_1:48; then ((i + 1) - j) + 1 = ((i + 1) -' j) + 1 by XREAL_0:def_2; then reconsider lj = ((len (Card g2)) - j) + 1 as Element of NAT by A4, A18, FINSEQ_3:29; (i + 1) - (((i + 1) - j) + 1) = 0 + (j - 1) ; then A23: (i + 1) - (((i + 1) - j) + 1) >= 0 by A16, XREAL_1:48; then A24: ((i + 1) -' lj) + 1 = (0 + (j - 1)) + 1 by A4, A19, XREAL_0:def_2 .= j ; ((i + 1) - j) + 1 >= 0 + 1 by A22, XREAL_1:6; then lj in Seg (i + 1) by A4, A19, A17, FINSEQ_1:1; then A25: g2 . lj = (((i + 2) -' lj) |-> <*(lj -' 1)*>) ^^ (Decomp (((i + 1) -' lj),2)) by A5, A6; A26: ((i + 1) -' lj) + 1 = ((i + 1) - lj) + 1 by A4, A19, A23, XREAL_0:def_2 .= (i + (1 + 1)) - lj ; A27: dom (((i + 2) -' lj) |-> <*(lj -' 1)*>) = Seg ((i + 2) -' lj) by FUNCOP_1:13 .= Seg j by A24, A26, XREAL_0:def_2 ; A28: dom (Decomp (((i + 1) -' lj),2)) = Seg (len (Decomp (((i + 1) -' lj),2))) by FINSEQ_1:def_3 .= Seg j by A24, Th9 ; Seg (len (g2 . lj)) = dom (g2 . lj) by FINSEQ_1:def_3 .= (Seg j) /\ (Seg j) by A25, A28, A27, PRE_POLY:def_4 .= Seg j ; then A29: len (g2 . lj) = j by FINSEQ_1:6; A30: dom (Decomp ((j -' 1),2)) = Seg (len (Decomp ((j -' 1),2))) by FINSEQ_1:def_3 .= Seg ((j -' 1) + 1) by Th9 .= Seg j by A16, XREAL_1:235 ; Seg (len (f2 . j)) = dom (f2 . j) by FINSEQ_1:def_3 .= (Seg j) /\ (Seg j) by A21, A30, A13, PRE_POLY:def_4 .= Seg j ; then A31: len (f2 . j) = j by FINSEQ_1:6; ((len (Card g2)) - j) + 1 in Seg (len g2) by A19, A20, FINSEQ_5:2; then A32: ((len (Card g2)) - j) + 1 in dom g2 by FINSEQ_1:def_3; j in dom f2 by A14, CARD_3:def_2; hence (Card f2) . j = j by A31, CARD_3:def_2 .= (Card g2) . (((len (Card g2)) - j) + 1) by A32, A29, CARD_3:def_2 .= (Rev (Card g2)) . j by A11, A14, FINSEQ_5:def_3 ; ::_thesis: verum end; len (Card f2) = len (Rev (Card g2)) by A11, FINSEQ_3:29; then A33: Card f2 = Rev (Card g2) by A12, FINSEQ_2:9; reconsider w = Card g2 as FinSequence of NAT ; A34: Seg (len (FlattenSeq f2)) = dom (FlattenSeq f2) by FINSEQ_1:def_3; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_(FlattenSeq_f2)_implies_y_in_rng_(FlattenSeq_g2)_)_&_(_y_in_rng_(FlattenSeq_g2)_implies_y_in_rng_(FlattenSeq_f2)_)_) let y be set ; ::_thesis: ( ( y in rng (FlattenSeq f2) implies y in rng (FlattenSeq g2) ) & ( y in rng (FlattenSeq g2) implies y in rng (FlattenSeq f2) ) ) thus ( y in rng (FlattenSeq f2) implies y in rng (FlattenSeq g2) ) ::_thesis: ( y in rng (FlattenSeq g2) implies y in rng (FlattenSeq f2) ) proof assume y in rng (FlattenSeq f2) ; ::_thesis: y in rng (FlattenSeq g2) then consider x being Nat such that A35: x in dom (FlattenSeq f2) and A36: (FlattenSeq f2) . x = y by FINSEQ_2:10; consider i1, j1 being Element of NAT such that A37: i1 in dom f2 and A38: j1 in dom (f2 . i1) and x = (Sum (Card (f2 | (i1 -' 1)))) + j1 and A39: (f2 . i1) . j1 = (FlattenSeq f2) . x by A35, PRE_POLY:29; A40: f2 . i1 = (Decomp ((i1 -' 1),2)) ^^ (i1 |-> <*((i + 1) -' i1)*>) by A2, A37; then j1 in (dom (Decomp ((i1 -' 1),2))) /\ (dom (i1 |-> <*((i + 1) -' i1)*>)) by A38, PRE_POLY:def_4; then j1 in dom (i1 |-> <*((i + 1) -' i1)*>) by XBOOLE_0:def_4; then A41: j1 in Seg i1 by FUNCOP_1:13; then A42: j1 <= i1 by FINSEQ_1:1; then A43: i1 - j1 >= 0 by XREAL_1:48; set j2 = (i1 -' j1) + 1; set i2 = j1; A44: dom (((i + 2) -' j1) |-> <*(j1 -' 1)*>) = Seg ((i + 2) -' j1) by FUNCOP_1:13; A45: i1 in Seg (i + 1) by A1, A37, FINSEQ_1:def_3; then A46: 1 <= i1 by FINSEQ_1:1; then A47: j1 in Seg ((i1 -' 1) + 1) by A41, XREAL_1:235; A48: i1 <= i + 1 by A45, FINSEQ_1:1; then A49: (i + 1) - i1 >= 0 by XREAL_1:48; A50: i + 1 >= j1 by A48, A42, XXREAL_0:2; then A51: (i + 1) - j1 >= 0 by XREAL_1:48; then A52: ((i + 1) -' j1) + 1 = ((i + 1) - j1) + 1 by XREAL_0:def_2 .= (i + (1 + 1)) - j1 ; (i + 1) -' j1 >= i1 -' j1 by A48, NAT_D:42; then ((i + 1) -' j1) + 1 >= (i1 -' j1) + 1 by XREAL_1:6; then (((i + 1) -' j1) + 1) - ((i1 -' j1) + 1) >= 0 by XREAL_1:48; then A53: (((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1) = (((i + 1) -' j1) + 1) - ((i1 -' j1) + 1) by XREAL_0:def_2 .= (((i + 1) -' j1) + 1) - ((i1 - j1) + 1) by A43, XREAL_0:def_2 .= (((i + 1) - j1) + 1) - ((1 - j1) + i1) by A51, XREAL_0:def_2 .= (i + 1) -' i1 by A49, XREAL_0:def_2 ; 1 <= j1 by A41, FINSEQ_1:1; then A54: j1 in Seg (i + 1) by A50, FINSEQ_1:1; then A55: g2 . j1 = (((i + 2) -' j1) |-> <*(j1 -' 1)*>) ^^ (Decomp (((i + 1) -' j1),2)) by A5, A6; i1 -' j1 <= (i + 1) -' j1 by A48, NAT_D:42; then ( 1 <= (i1 -' j1) + 1 & (i1 -' j1) + 1 <= ((i + 1) -' j1) + 1 ) by NAT_1:11, XREAL_1:6; then A56: (i1 -' j1) + 1 in Seg (((i + 1) -' j1) + 1) by FINSEQ_1:1; then A57: (i1 -' j1) + 1 in Seg ((i + 2) -' j1) by A52, XREAL_0:def_2; dom (Decomp (((i + 1) -' j1),2)) = Seg (len (Decomp (((i + 1) -' j1),2))) by FINSEQ_1:def_3 .= Seg (((i + 1) -' j1) + 1) by Th9 .= Seg ((i + 2) -' j1) by A52, XREAL_0:def_2 ; then dom (g2 . j1) = (Seg ((i + 2) -' j1)) /\ (Seg ((i + 2) -' j1)) by A55, A44, PRE_POLY:def_4; then A58: (i1 -' j1) + 1 in dom (g2 . j1) by A56, A52, XREAL_0:def_2; then A59: (g2 . j1) . ((i1 -' j1) + 1) = ((((i + 2) -' j1) |-> <*(j1 -' 1)*>) . ((i1 -' j1) + 1)) ^ ((Decomp (((i + 1) -' j1),2)) . ((i1 -' j1) + 1)) by A55, PRE_POLY:def_4 .= <*(j1 -' 1)*> ^ ((Decomp (((i + 1) -' j1),2)) . ((i1 -' j1) + 1)) by A57, FUNCOP_1:7 .= <*(j1 -' 1)*> ^ <*(((i1 -' j1) + 1) -' 1),((((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1))*> by A56, Th14 .= <*(j1 -' 1),(((i1 -' j1) + 1) -' 1),((((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1))*> by FINSEQ_1:43 .= <*(j1 -' 1),(i1 -' j1),((i + 1) -' i1)*> by A53, NAT_D:34 ; j1 in dom g2 by A4, A54, FINSEQ_1:def_3; then A60: ( (Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1) in dom (FlattenSeq g2) & (g2 . j1) . ((i1 -' j1) + 1) = (FlattenSeq g2) . ((Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1)) ) by A58, PRE_POLY:30; y = ((Decomp ((i1 -' 1),2)) . j1) ^ ((i1 |-> <*((i + 1) -' i1)*>) . j1) by A36, A38, A39, A40, PRE_POLY:def_4 .= ((Decomp ((i1 -' 1),2)) . j1) ^ <*((i + 1) -' i1)*> by A41, FUNCOP_1:7 .= <*(j1 -' 1),(((i1 -' 1) + 1) -' j1)*> ^ <*((i + 1) -' i1)*> by A47, Th14 .= <*(j1 -' 1),(i1 -' j1)*> ^ <*((i + 1) -' i1)*> by A46, XREAL_1:235 .= <*(j1 -' 1),(i1 -' j1),((i + 1) -' i1)*> by FINSEQ_1:43 ; hence y in rng (FlattenSeq g2) by A59, A60, FUNCT_1:def_3; ::_thesis: verum end; assume y in rng (FlattenSeq g2) ; ::_thesis: y in rng (FlattenSeq f2) then consider x being Nat such that A61: x in dom (FlattenSeq g2) and A62: (FlattenSeq g2) . x = y by FINSEQ_2:10; consider i1, j1 being Element of NAT such that A63: i1 in dom g2 and A64: j1 in dom (g2 . i1) and x = (Sum (Card (g2 | (i1 -' 1)))) + j1 and A65: (g2 . i1) . j1 = (FlattenSeq g2) . x by A61, PRE_POLY:29; A66: g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp (((i + 1) -' i1),2)) by A5, A63; then j1 in (dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>)) /\ (dom (Decomp (((i + 1) -' i1),2))) by A64, PRE_POLY:def_4; then j1 in dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>) by XBOOLE_0:def_4; then A67: j1 in Seg ((i + 2) -' i1) by FUNCOP_1:13; then j1 >= 1 by FINSEQ_1:1; then A68: j1 - 1 >= 0 by XREAL_1:48; A69: i1 in Seg (i + 1) by A4, A63, FINSEQ_1:def_3; then i1 <= i + 1 by FINSEQ_1:1; then A70: (i + 1) - i1 >= 0 by XREAL_1:48; then ((i + 1) -' i1) + 1 = ((i + 1) - i1) + 1 by XREAL_0:def_2 .= (i + (1 + 1)) - i1 ; then A71: j1 in Seg (((i + 1) -' i1) + 1) by A67, XREAL_0:def_2; then A72: j1 <= ((i + 1) -' i1) + 1 by FINSEQ_1:1; then A73: (((i + 1) -' i1) + 1) - j1 >= 0 by XREAL_1:48; j1 <= ((i + 1) - i1) + 1 by A70, A72, XREAL_0:def_2; then j1 - 1 <= (i + 1) - i1 by XREAL_1:20; then A74: (j1 - 1) + i1 <= i + 1 by XREAL_1:19; then A75: (j1 -' 1) + i1 <= i + 1 by A68, XREAL_0:def_2; (i + 1) - ((j1 - 1) + i1) >= 0 by A74, XREAL_1:48; then (i + 1) - ((j1 -' 1) + i1) >= 0 by A68, XREAL_0:def_2; then A76: (i + 1) -' ((j1 -' 1) + i1) = (i + 1) - ((j1 -' 1) + i1) by XREAL_0:def_2 .= (i + 1) - ((j1 - 1) + i1) by A68, XREAL_0:def_2 .= (((i + 1) - i1) + 1) - j1 .= (((i + 1) -' i1) + 1) - j1 by A70, XREAL_0:def_2 .= (((i + 1) -' i1) + 1) -' j1 by A73, XREAL_0:def_2 ; A77: y = ((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A62, A64, A65, A66, PRE_POLY:def_4 .= <*(i1 -' 1)*> ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A67, FUNCOP_1:7 .= <*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by A71, Th14 .= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by FINSEQ_1:43 ; set j2 = i1; set i2 = (j1 -' 1) + i1; A78: (j1 -' 1) + i1 >= i1 by NAT_1:11; A79: dom (((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) = Seg ((j1 -' 1) + i1) by FUNCOP_1:13; A80: 1 <= i1 by A69, FINSEQ_1:1; then A81: i1 in Seg ((j1 -' 1) + i1) by A78, FINSEQ_1:1; then A82: i1 in Seg ((((j1 -' 1) + i1) -' 1) + 1) by A80, A78, XREAL_1:235, XXREAL_0:2; (j1 -' 1) + i1 >= 1 by A80, A78, XXREAL_0:2; then A83: (j1 -' 1) + i1 in Seg (i + 1) by A75, FINSEQ_1:1; then A84: f2 . ((j1 -' 1) + i1) = (Decomp ((((j1 -' 1) + i1) -' 1),2)) ^^ (((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) by A2, A3; dom (Decomp ((((j1 -' 1) + i1) -' 1),2)) = Seg (len (Decomp ((((j1 -' 1) + i1) -' 1),2))) by FINSEQ_1:def_3 .= Seg ((((j1 -' 1) + i1) -' 1) + 1) by Th9 .= Seg ((j1 -' 1) + i1) by A80, A78, XREAL_1:235, XXREAL_0:2 ; then dom (f2 . ((j1 -' 1) + i1)) = (Seg ((j1 -' 1) + i1)) /\ (Seg ((j1 -' 1) + i1)) by A84, A79, PRE_POLY:def_4; then A85: i1 in dom (f2 . ((j1 -' 1) + i1)) by A80, A78, FINSEQ_1:1; (j1 -' 1) + i1 in dom f2 by A1, A83, FINSEQ_1:def_3; then A86: ( (Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1 in dom (FlattenSeq f2) & (f2 . ((j1 -' 1) + i1)) . i1 = (FlattenSeq f2) . ((Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1) ) by A85, PRE_POLY:30; (f2 . ((j1 -' 1) + i1)) . i1 = ((Decomp ((((j1 -' 1) + i1) -' 1),2)) . i1) ^ ((((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) . i1) by A84, A85, PRE_POLY:def_4 .= ((Decomp ((((j1 -' 1) + i1) -' 1),2)) . i1) ^ <*((i + 1) -' ((j1 -' 1) + i1))*> by A81, FUNCOP_1:7 .= <*(i1 -' 1),(((((j1 -' 1) + i1) -' 1) + 1) -' i1)*> ^ <*((i + 1) -' ((j1 -' 1) + i1))*> by A82, Th14 .= <*(i1 -' 1),(((((j1 -' 1) + i1) -' 1) + 1) -' i1),((i + 1) -' ((j1 -' 1) + i1))*> by FINSEQ_1:43 .= <*(i1 -' 1),(((j1 -' 1) + i1) -' i1),((i + 1) -' ((j1 -' 1) + i1))*> by A80, A78, XREAL_1:235, XXREAL_0:2 .= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by A76, NAT_D:34 ; hence y in rng (FlattenSeq f2) by A77, A86, FUNCT_1:def_3; ::_thesis: verum end; then A87: rng (FlattenSeq f2) = rng (FlattenSeq g2) by TARSKI:1; now__::_thesis:_for_x,_y_being_set_st_x_in_dom_(FlattenSeq_g2)_&_y_in_dom_(FlattenSeq_g2)_&_(FlattenSeq_g2)_._x_=_(FlattenSeq_g2)_._y_holds_ x_=_y A88: (i + 1) + 1 >= i + 1 by NAT_1:11; let x, y be set ; ::_thesis: ( x in dom (FlattenSeq g2) & y in dom (FlattenSeq g2) & (FlattenSeq g2) . x = (FlattenSeq g2) . y implies x = y ) assume that A89: x in dom (FlattenSeq g2) and A90: y in dom (FlattenSeq g2) and A91: (FlattenSeq g2) . x = (FlattenSeq g2) . y ; ::_thesis: x = y consider i1, j1 being Element of NAT such that A92: i1 in dom g2 and A93: j1 in dom (g2 . i1) and A94: x = (Sum (Card (g2 | (i1 -' 1)))) + j1 and A95: (g2 . i1) . j1 = (FlattenSeq g2) . x by A89, PRE_POLY:29; A96: g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp (((i + 1) -' i1),2)) by A5, A92; i1 in Seg (i + 1) by A4, A92, FINSEQ_1:def_3; then A97: i1 <= i + 1 by FINSEQ_1:1; then (i + 1) + 1 >= i1 by A88, XXREAL_0:2; then A98: (i + 2) - i1 >= 0 by XREAL_1:48; (i + 1) - i1 >= 0 by A97, XREAL_1:48; then A99: ((i + 1) -' i1) + 1 = ((i + 1) - i1) + 1 by XREAL_0:def_2 .= (i + 2) -' i1 by A98, XREAL_0:def_2 ; A100: dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>) = Seg ((i + 2) -' i1) by FUNCOP_1:13; dom (Decomp (((i + 1) -' i1),2)) = Seg (len (Decomp (((i + 1) -' i1),2))) by FINSEQ_1:def_3 .= Seg ((i + 2) -' i1) by A99, Th9 ; then A101: dom (g2 . i1) = (Seg ((i + 2) -' i1)) /\ (Seg ((i + 2) -' i1)) by A96, A100, PRE_POLY:def_4 .= Seg ((i + 2) -' i1) ; j1 in Seg (len (g2 . i1)) by A93, FINSEQ_1:def_3; then A102: j1 >= 1 by FINSEQ_1:1; consider i2, j2 being Element of NAT such that A103: i2 in dom g2 and A104: j2 in dom (g2 . i2) and A105: y = (Sum (Card (g2 | (i2 -' 1)))) + j2 and A106: (g2 . i2) . j2 = (FlattenSeq g2) . y by A90, PRE_POLY:29; A107: g2 . i2 = (((i + 2) -' i2) |-> <*(i2 -' 1)*>) ^^ (Decomp (((i + 1) -' i2),2)) by A5, A103; i2 in Seg (i + 1) by A4, A103, FINSEQ_1:def_3; then A108: i2 <= i + 1 by FINSEQ_1:1; then (i + 1) + 1 >= i2 by A88, XXREAL_0:2; then A109: (i + 2) - i2 >= 0 by XREAL_1:48; (i + 1) - i2 >= 0 by A108, XREAL_1:48; then A110: ((i + 1) -' i2) + 1 = ((i + 1) - i2) + 1 by XREAL_0:def_2 .= (i + 2) -' i2 by A109, XREAL_0:def_2 ; A111: dom (((i + 2) -' i2) |-> <*(i2 -' 1)*>) = Seg ((i + 2) -' i2) by FUNCOP_1:13; dom (Decomp (((i + 1) -' i2),2)) = Seg (len (Decomp (((i + 1) -' i2),2))) by FINSEQ_1:def_3 .= Seg ((i + 2) -' i2) by A110, Th9 ; then A112: dom (g2 . i2) = (Seg ((i + 2) -' i2)) /\ (Seg ((i + 2) -' i2)) by A107, A111, PRE_POLY:def_4 .= Seg ((i + 2) -' i2) ; A113: (g2 . i2) . j2 = ((((i + 2) -' i2) |-> <*(i2 -' 1)*>) . j2) ^ ((Decomp (((i + 1) -' i2),2)) . j2) by A104, A107, PRE_POLY:def_4 .= <*(i2 -' 1)*> ^ ((Decomp (((i + 1) -' i2),2)) . j2) by A104, A112, FUNCOP_1:7 .= <*(i2 -' 1)*> ^ <*(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*> by A104, A110, A112, Th14 .= <*(i2 -' 1),(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*> by FINSEQ_1:43 ; j2 in Seg (len (g2 . i2)) by A104, FINSEQ_1:def_3; then A114: j2 >= 1 by FINSEQ_1:1; (g2 . i1) . j1 = ((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A93, A96, PRE_POLY:def_4 .= <*(i1 -' 1)*> ^ ((Decomp (((i + 1) -' i1),2)) . j1) by A93, A101, FUNCOP_1:7 .= <*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by A93, A99, A101, Th14 .= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by FINSEQ_1:43 ; then ( i1 -' 1 = i2 -' 1 & j1 -' 1 = j2 -' 1 ) by A91, A95, A106, A113, FINSEQ_1:78; hence x = y by A94, A105, A102, A114, XREAL_1:234; ::_thesis: verum end; then A115: FlattenSeq g2 is one-to-one by FUNCT_1:def_4; len (FlattenSeq f2) = Sum (Card f2) by PRE_POLY:27 .= Sum w by A33, Th3 .= len (FlattenSeq g2) by PRE_POLY:27 ; then FlattenSeq f2 is one-to-one by A87, A115, FINSEQ_4:61; then FlattenSeq f2, FlattenSeq g2 are_fiberwise_equipotent by A87, A115, RFINSEQ:26; then consider P being Permutation of (dom (FlattenSeq g2)) such that A116: FlattenSeq f2 = (FlattenSeq g2) * P by RFINSEQ:4; A117: dom (Card g2) = dom g2 by CARD_3:def_2; then A118: len (Card g2) = len g2 by FINSEQ_3:29; consider r1 being FinSequence of the carrier of L such that A119: len r1 = i + 1 and A120: ((p *' q) *' r) . i = Sum r1 and A121: for k being Element of NAT st k in dom r1 holds r1 . k = ((p *' q) . (k -' 1)) * (r . ((i + 1) -' k)) by Def9; A122: dom r1 = Seg (i + 1) by A119, FINSEQ_1:def_3; deffunc H3( Nat) -> Element of the carrier of L * = prodTuples (p,q,r,(f2 /. $1)); consider f1 being FinSequence of the carrier of L * such that A123: len f1 = len f2 and A124: for k being Nat st k in dom f1 holds f1 . k = H3(k) from FINSEQ_2:sch_1(); A125: dom f1 = Seg (len f2) by A123, FINSEQ_1:def_3; A126: now__::_thesis:_for_j_being_Nat_st_j_in_dom_r1_holds_ r1_._j_=_(Sum_f1)_._j let j be Nat; ::_thesis: ( j in dom r1 implies r1 . j = (Sum f1) . j ) A127: dom (j |-> <*((i + 1) -' j)*>) = Seg j by FUNCOP_1:13; consider r3 being FinSequence of the carrier of L such that A128: len r3 = (j -' 1) + 1 and A129: (p *' q) . (j -' 1) = Sum r3 and A130: for k being Element of NAT st k in dom r3 holds r3 . k = (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k)) by Def9; assume A131: j in dom r1 ; ::_thesis: r1 . j = (Sum f1) . j then A132: 1 <= j by A122, FINSEQ_1:1; then A133: len r3 = j by A128, XREAL_1:235; len (Decomp ((j -' 1),2)) = (j -' 1) + 1 by Th9 .= j by A132, XREAL_1:235 ; then A134: dom (Decomp ((j -' 1),2)) = Seg j by FINSEQ_1:def_3; A135: dom r1 = dom f1 by A119, A1, A123, FINSEQ_3:29; then A136: f1 /. j = f1 . j by A131, PARTFUN1:def_6 .= prodTuples (p,q,r,(f2 /. j)) by A1, A124, A125, A122, A131 ; dom f1 = dom f2 by A123, FINSEQ_3:29; then A137: f2 /. j = f2 . j by A131, A135, PARTFUN1:def_6 .= (Decomp ((j -' 1),2)) ^^ (j |-> <*((i + 1) -' j)*>) by A2, A3, A122, A131 ; then A138: dom (f2 /. j) = (dom (Decomp ((j -' 1),2))) /\ (dom (j |-> <*((i + 1) -' j)*>)) by PRE_POLY:def_4 .= Seg j by A134, A127 ; A139: len (prodTuples (p,q,r,(f2 /. j))) = len (f2 /. j) by Def5 .= j by A131, A138, FINSEQ_1:def_3 ; then A140: dom (prodTuples (p,q,r,(f2 /. j))) = Seg j by FINSEQ_1:def_3; A141: dom (r3 * (r . ((i + 1) -' j))) = dom r3 by POLYNOM1:def_2; A142: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(prodTuples_(p,q,r,(f2_/._j)))_holds_ (prodTuples_(p,q,r,(f2_/._j)))_._k_=_(r3_*_(r_._((i_+_1)_-'_j)))_._k let k be Nat; ::_thesis: ( k in dom (prodTuples (p,q,r,(f2 /. j))) implies (prodTuples (p,q,r,(f2 /. j))) . k = (r3 * (r . ((i + 1) -' j))) . k ) assume A143: k in dom (prodTuples (p,q,r,(f2 /. j))) ; ::_thesis: (prodTuples (p,q,r,(f2 /. j))) . k = (r3 * (r . ((i + 1) -' j))) . k then A144: (f2 /. j) /. k = (f2 /. j) . k by A138, A140, PARTFUN1:def_6 .= ((Decomp ((j -' 1),2)) . k) ^ ((j |-> <*((i + 1) -' j)*>) . k) by A137, A138, A140, A143, PRE_POLY:def_4 .= <*(k -' 1),(((j -' 1) + 1) -' k)*> ^ ((j |-> <*((i + 1) -' j)*>) . k) by A128, A133, A140, A143, Th14 .= <*(k -' 1),(((j -' 1) + 1) -' k)*> ^ <*((i + 1) -' j)*> by A140, A143, FUNCOP_1:7 .= <*(k -' 1),(((j -' 1) + 1) -' k),((i + 1) -' j)*> by FINSEQ_1:43 ; 1 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1; then 1 in Seg (len ((f2 /. j) /. k)) by A144, FINSEQ_1:45; then 1 in dom ((f2 /. j) /. k) by FINSEQ_1:def_3; then A145: ((f2 /. j) /. k) /. 1 = ((f2 /. j) /. k) . 1 by PARTFUN1:def_6 .= k -' 1 by A144, FINSEQ_1:45 ; A146: k in dom r3 by A133, A140, A143, FINSEQ_1:def_3; then A147: r3 /. k = r3 . k by PARTFUN1:def_6 .= (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k)) by A130, A146 ; 3 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1; then 3 in Seg (len ((f2 /. j) /. k)) by A144, FINSEQ_1:45; then 3 in dom ((f2 /. j) /. k) by FINSEQ_1:def_3; then A148: ((f2 /. j) /. k) /. 3 = ((f2 /. j) /. k) . 3 by PARTFUN1:def_6 .= (i + 1) -' j by A144, FINSEQ_1:45 ; 2 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1; then 2 in Seg (len ((f2 /. j) /. k)) by A144, FINSEQ_1:45; then 2 in dom ((f2 /. j) /. k) by FINSEQ_1:def_3; then A149: ((f2 /. j) /. k) /. 2 = ((f2 /. j) /. k) . 2 by PARTFUN1:def_6 .= ((j -' 1) + 1) -' k by A144, FINSEQ_1:45 ; thus (prodTuples (p,q,r,(f2 /. j))) . k = ((p . (((f2 /. j) /. k) /. 1)) * (q . (((f2 /. j) /. k) /. 2))) * (r . (((f2 /. j) /. k) /. 3)) by A138, A140, A143, Def5 .= (r3 * (r . ((i + 1) -' j))) /. k by A146, A147, A145, A149, A148, POLYNOM1:def_2 .= (r3 * (r . ((i + 1) -' j))) . k by A141, A146, PARTFUN1:def_6 ; ::_thesis: verum end; len f1 = len (Sum f1) by MATRLIN:def_6; then A150: dom f1 = dom (Sum f1) by FINSEQ_3:29; len (r3 * (r . ((i + 1) -' j))) = len r3 by A141, FINSEQ_3:29; then A151: prodTuples (p,q,r,(f2 /. j)) = r3 * (r . ((i + 1) -' j)) by A139, A133, A142, FINSEQ_2:9; ((p *' q) . (j -' 1)) * (r . ((i + 1) -' j)) = Sum (r3 * (r . ((i + 1) -' j))) by A129, POLYNOM1:13; hence r1 . j = Sum (r3 * (r . ((i + 1) -' j))) by A121, A131 .= (Sum f1) /. j by A131, A150, A135, A136, A151, MATRLIN:def_6 .= (Sum f1) . j by A131, A150, A135, PARTFUN1:def_6 ; ::_thesis: verum end; deffunc H4( Nat) -> Element of the carrier of L * = prodTuples (p,q,r,(g2 /. $1)); consider g1 being FinSequence of the carrier of L * such that A152: len g1 = len g2 and A153: for k being Nat st k in dom g1 holds g1 . k = H4(k) from FINSEQ_2:sch_1(); A154: dom g1 = Seg (len g2) by A152, FINSEQ_1:def_3; A155: now__::_thesis:_for_j_being_Nat_st_j_in_dom_r2_holds_ r2_._j_=_(Sum_g1)_._j let j be Nat; ::_thesis: ( j in dom r2 implies r2 . j = (Sum g1) . j ) A156: dom (((i + 2) -' j) |-> <*(j -' 1)*>) = Seg ((i + 2) -' j) by FUNCOP_1:13; consider r3 being FinSequence of the carrier of L such that A157: len r3 = ((i + 1) -' j) + 1 and A158: (q *' r) . ((i + 1) -' j) = Sum r3 and A159: for k being Element of NAT st k in dom r3 holds r3 . k = (q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k)) by Def9; assume A160: j in dom r2 ; ::_thesis: r2 . j = (Sum g1) . j then A161: j <= i + 1 by A10, FINSEQ_1:1; (i + 1) + 1 >= i + 1 by NAT_1:11; then (i + 1) + 1 >= j by A161, XXREAL_0:2; then A162: (i + 2) - j >= 0 by XREAL_1:48; (i + 1) - j >= 0 by A161, XREAL_1:48; then A163: ((i + 1) -' j) + 1 = ((i + 1) - j) + 1 by XREAL_0:def_2 .= (i + 2) -' j by A162, XREAL_0:def_2 ; then len (Decomp (((i + 1) -' j),2)) = (i + 2) -' j by Th9; then A164: dom (Decomp (((i + 1) -' j),2)) = Seg ((i + 2) -' j) by FINSEQ_1:def_3; A165: dom r2 = dom g1 by A7, A4, A152, FINSEQ_3:29; then A166: g1 /. j = g1 . j by A160, PARTFUN1:def_6 .= prodTuples (p,q,r,(g2 /. j)) by A4, A153, A154, A10, A160 ; dom g1 = dom g2 by A152, FINSEQ_3:29; then A167: g2 /. j = g2 . j by A160, A165, PARTFUN1:def_6 .= (((i + 2) -' j) |-> <*(j -' 1)*>) ^^ (Decomp (((i + 1) -' j),2)) by A5, A6, A10, A160 ; then A168: dom (g2 /. j) = (dom (((i + 2) -' j) |-> <*(j -' 1)*>)) /\ (dom (Decomp (((i + 1) -' j),2))) by PRE_POLY:def_4 .= Seg ((i + 2) -' j) by A164, A156 ; A169: len (prodTuples (p,q,r,(g2 /. j))) = len (g2 /. j) by Def5 .= (i + 2) -' j by A168, FINSEQ_1:def_3 ; then A170: dom (prodTuples (p,q,r,(g2 /. j))) = Seg ((i + 2) -' j) by FINSEQ_1:def_3; A171: dom ((p . (j -' 1)) * r3) = dom r3 by POLYNOM1:def_1; A172: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(prodTuples_(p,q,r,(g2_/._j)))_holds_ (prodTuples_(p,q,r,(g2_/._j)))_._k_=_((p_._(j_-'_1))_*_r3)_._k let k be Nat; ::_thesis: ( k in dom (prodTuples (p,q,r,(g2 /. j))) implies (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (j -' 1)) * r3) . k ) assume A173: k in dom (prodTuples (p,q,r,(g2 /. j))) ; ::_thesis: (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (j -' 1)) * r3) . k then A174: (g2 /. j) /. k = (g2 /. j) . k by A168, A170, PARTFUN1:def_6 .= ((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ ((Decomp (((i + 1) -' j),2)) . k) by A167, A168, A170, A173, PRE_POLY:def_4 .= ((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*> by A163, A170, A173, Th14 .= <*(j -' 1)*> ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*> by A170, A173, FUNCOP_1:7 .= <*(j -' 1),(k -' 1),((((i + 1) -' j) + 1) -' k)*> by FINSEQ_1:43 ; 1 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1; then 1 in Seg (len ((g2 /. j) /. k)) by A174, FINSEQ_1:45; then 1 in dom ((g2 /. j) /. k) by FINSEQ_1:def_3; then A175: ((g2 /. j) /. k) /. 1 = ((g2 /. j) /. k) . 1 by PARTFUN1:def_6 .= j -' 1 by A174, FINSEQ_1:45 ; A176: k in dom r3 by A157, A163, A170, A173, FINSEQ_1:def_3; then A177: r3 /. k = r3 . k by PARTFUN1:def_6 .= (q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k)) by A159, A176 ; 3 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1; then 3 in Seg (len ((g2 /. j) /. k)) by A174, FINSEQ_1:45; then 3 in dom ((g2 /. j) /. k) by FINSEQ_1:def_3; then A178: ((g2 /. j) /. k) /. 3 = ((g2 /. j) /. k) . 3 by PARTFUN1:def_6 .= (((i + 1) -' j) + 1) -' k by A174, FINSEQ_1:45 ; 2 in Seg 3 by ENUMSET1:def_1, FINSEQ_3:1; then 2 in Seg (len ((g2 /. j) /. k)) by A174, FINSEQ_1:45; then 2 in dom ((g2 /. j) /. k) by FINSEQ_1:def_3; then A179: ((g2 /. j) /. k) /. 2 = ((g2 /. j) /. k) . 2 by PARTFUN1:def_6 .= k -' 1 by A174, FINSEQ_1:45 ; thus (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (((g2 /. j) /. k) /. 1)) * (q . (((g2 /. j) /. k) /. 2))) * (r . (((g2 /. j) /. k) /. 3)) by A168, A170, A173, Def5 .= (p . (((g2 /. j) /. k) /. 1)) * ((q . (((g2 /. j) /. k) /. 2)) * (r . (((g2 /. j) /. k) /. 3))) by GROUP_1:def_3 .= ((p . (j -' 1)) * r3) /. k by A176, A177, A175, A179, A178, POLYNOM1:def_1 .= ((p . (j -' 1)) * r3) . k by A171, A176, PARTFUN1:def_6 ; ::_thesis: verum end; len g1 = len (Sum g1) by MATRLIN:def_6; then A180: dom g1 = dom (Sum g1) by FINSEQ_3:29; len ((p . (j -' 1)) * r3) = len r3 by A171, FINSEQ_3:29; then A181: prodTuples (p,q,r,(g2 /. j)) = (p . (j -' 1)) * r3 by A157, A163, A169, A172, FINSEQ_2:9; (p . (j -' 1)) * ((q *' r) . ((i + 1) -' j)) = Sum ((p . (j -' 1)) * r3) by A158, POLYNOM1:12; hence r2 . j = Sum ((p . (j -' 1)) * r3) by A9, A160 .= (Sum g1) /. j by A160, A180, A165, A166, A181, MATRLIN:def_6 .= (Sum g1) . j by A160, A180, A165, PARTFUN1:def_6 ; ::_thesis: verum end; A182: dom (Card g2) = Seg (i + 1) by A4, A117, FINSEQ_1:def_3; A183: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_g2)_holds_ (Card_g2)_._j_=_(Card_g1)_._j let j be Nat; ::_thesis: ( j in dom (Card g2) implies (Card g2) . j = (Card g1) . j ) assume A184: j in dom (Card g2) ; ::_thesis: (Card g2) . j = (Card g1) . j then A185: j in dom g1 by A4, A152, A182, FINSEQ_1:def_3; g1 . j = prodTuples (p,q,r,(g2 /. j)) by A4, A153, A154, A182, A184; then A186: len (g1 . j) = len (g2 /. j) by Def5 .= len (g2 . j) by A117, A184, PARTFUN1:def_6 ; thus (Card g2) . j = len (g2 . j) by A117, A184, CARD_3:def_2 .= (Card g1) . j by A185, A186, CARD_3:def_2 ; ::_thesis: verum end; A187: dom (Card g1) = dom g1 by CARD_3:def_2; then len (Card g1) = len g1 by FINSEQ_3:29; then A188: Card g2 = Card g1 by A152, A118, A183, FINSEQ_2:9; then A189: len (FlattenSeq g2) = len (FlattenSeq g1) by PRE_POLY:28; then A190: dom (FlattenSeq g2) = dom (FlattenSeq g1) by FINSEQ_3:29; then reconsider P = P as Permutation of (dom (FlattenSeq g1)) ; A191: dom (FlattenSeq g1) = Seg (len (FlattenSeq g1)) by FINSEQ_1:def_3; A192: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(FlattenSeq_g1)_holds_ (FlattenSeq_g1)_._j_=_(prodTuples_(p,q,r,(FlattenSeq_g2)))_._j let j be Nat; ::_thesis: ( j in dom (FlattenSeq g1) implies (FlattenSeq g1) . j = (prodTuples (p,q,r,(FlattenSeq g2))) . j ) assume A193: j in dom (FlattenSeq g1) ; ::_thesis: (FlattenSeq g1) . j = (prodTuples (p,q,r,(FlattenSeq g2))) . j then consider i1, j1 being Element of NAT such that A194: i1 in dom g1 and A195: j1 in dom (g1 . i1) and A196: j = (Sum (Card (g1 | (i1 -' 1)))) + j1 and A197: (g1 . i1) . j1 = (FlattenSeq g1) . j by PRE_POLY:29; A198: j in dom (FlattenSeq g2) by A189, A191, A193, FINSEQ_1:def_3; then consider i2, j2 being Element of NAT such that A199: ( i2 in dom g2 & j2 in dom (g2 . i2) ) and A200: j = (Sum (Card (g2 | (i2 -' 1)))) + j2 and A201: (g2 . i2) . j2 = (FlattenSeq g2) . j by PRE_POLY:29; (Sum ((Card g1) | (i1 -' 1))) + j1 = (Sum (Card (g1 | (i1 -' 1)))) + j1 by Th16 .= (Sum ((Card g2) | (i2 -' 1))) + j2 by A196, A200, Th16 ; then A202: ( i1 = i2 & j1 = j2 ) by A188, A194, A195, A199, Th22; i1 in Seg (len g2) by A152, A194, FINSEQ_1:def_3; then A203: i1 in dom g2 by FINSEQ_1:def_3; A204: g1 . i1 = prodTuples (p,q,r,(g2 /. i1)) by A153, A194; then len (g1 . i1) = len (g2 /. i1) by Def5 .= len (g2 . i1) by A187, A117, A188, A194, PARTFUN1:def_6 ; then j1 in Seg (len (g2 . i1)) by A195, FINSEQ_1:def_3; then A205: j1 in Seg (len (g2 /. i1)) by A203, PARTFUN1:def_6; then j1 in dom (g2 /. i1) by FINSEQ_1:def_3; then A206: (g2 /. i1) /. j1 = (g2 /. i1) . j1 by PARTFUN1:def_6 .= (g2 . i1) . j1 by A203, PARTFUN1:def_6 .= (FlattenSeq g2) /. j by A198, A201, A202, PARTFUN1:def_6 ; Seg (len (g2 /. i1)) = dom (g2 /. i1) by FINSEQ_1:def_3; hence (FlattenSeq g1) . j = ((p . (((g2 /. i1) /. j1) /. 1)) * (q . (((g2 /. i1) /. j1) /. 2))) * (r . (((g2 /. i1) /. j1) /. 3)) by A197, A204, A205, Def5 .= (prodTuples (p,q,r,(FlattenSeq g2))) . j by A190, A193, A206, Def5 ; ::_thesis: verum end; A207: dom (Card f2) = dom f2 by CARD_3:def_2; then A208: len (Card f2) = len f2 by FINSEQ_3:29; A209: dom (Card f2) = Seg (i + 1) by A1, A207, FINSEQ_1:def_3; A210: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Card_f2)_holds_ (Card_f2)_._j_=_(Card_f1)_._j let j be Nat; ::_thesis: ( j in dom (Card f2) implies (Card f2) . j = (Card f1) . j ) assume A211: j in dom (Card f2) ; ::_thesis: (Card f2) . j = (Card f1) . j then A212: j in dom f1 by A1, A123, A209, FINSEQ_1:def_3; f1 . j = prodTuples (p,q,r,(f2 /. j)) by A1, A124, A125, A209, A211; then A213: len (f1 . j) = len (f2 /. j) by Def5 .= len (f2 . j) by A207, A211, PARTFUN1:def_6 ; thus (Card f2) . j = len (f2 . j) by A207, A211, CARD_3:def_2 .= (Card f1) . j by A212, A213, CARD_3:def_2 ; ::_thesis: verum end; A214: dom (Card f1) = dom f1 by CARD_3:def_2; then len (Card f1) = len f1 by FINSEQ_3:29; then A215: Card f2 = Card f1 by A123, A208, A210, FINSEQ_2:9; then A216: len (FlattenSeq f1) = len (FlattenSeq f2) by PRE_POLY:28; A217: Seg (len (FlattenSeq f1)) = dom (FlattenSeq f1) by FINSEQ_1:def_3; A218: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(FlattenSeq_f1)_holds_ (FlattenSeq_f1)_._j_=_(prodTuples_(p,q,r,(FlattenSeq_f2)))_._j let j be Nat; ::_thesis: ( j in dom (FlattenSeq f1) implies (FlattenSeq f1) . j = (prodTuples (p,q,r,(FlattenSeq f2))) . j ) assume A219: j in dom (FlattenSeq f1) ; ::_thesis: (FlattenSeq f1) . j = (prodTuples (p,q,r,(FlattenSeq f2))) . j then consider i1, j1 being Element of NAT such that A220: i1 in dom f1 and A221: j1 in dom (f1 . i1) and A222: j = (Sum (Card (f1 | (i1 -' 1)))) + j1 and A223: (f1 . i1) . j1 = (FlattenSeq f1) . j by PRE_POLY:29; A224: j in dom (FlattenSeq f2) by A216, A34, A219, FINSEQ_1:def_3; then consider i2, j2 being Element of NAT such that A225: ( i2 in dom f2 & j2 in dom (f2 . i2) ) and A226: j = (Sum (Card (f2 | (i2 -' 1)))) + j2 and A227: (f2 . i2) . j2 = (FlattenSeq f2) . j by PRE_POLY:29; (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum (Card (f1 | (i1 -' 1)))) + j1 by Th16 .= (Sum ((Card f2) | (i2 -' 1))) + j2 by A222, A226, Th16 ; then A228: ( i1 = i2 & j1 = j2 ) by A215, A220, A221, A225, Th22; i1 in Seg (len f2) by A123, A220, FINSEQ_1:def_3; then A229: i1 in dom f2 by FINSEQ_1:def_3; A230: f1 . i1 = prodTuples (p,q,r,(f2 /. i1)) by A124, A220; then len (f1 . i1) = len (f2 /. i1) by Def5 .= len (f2 . i1) by A214, A207, A215, A220, PARTFUN1:def_6 ; then j1 in Seg (len (f2 . i1)) by A221, FINSEQ_1:def_3; then A231: j1 in Seg (len (f2 /. i1)) by A229, PARTFUN1:def_6; then j1 in dom (f2 /. i1) by FINSEQ_1:def_3; then A232: (f2 /. i1) /. j1 = (f2 /. i1) . j1 by PARTFUN1:def_6 .= (f2 . i1) . j1 by A229, PARTFUN1:def_6 .= (FlattenSeq f2) /. j by A224, A227, A228, PARTFUN1:def_6 ; Seg (len (f2 /. i1)) = dom (f2 /. i1) by FINSEQ_1:def_3; hence (FlattenSeq f1) . j = ((p . (((f2 /. i1) /. j1) /. 1)) * (q . (((f2 /. i1) /. j1) /. 2))) * (r . (((f2 /. i1) /. j1) /. 3)) by A223, A230, A231, Def5 .= ((p . (((FlattenSeq f2) /. j) /. 1)) * (q . (((FlattenSeq f2) /. j) /. 2))) * (r . (((FlattenSeq f2) /. j) /. 3)) by A232 .= (prodTuples (p,q,r,(FlattenSeq f2))) . j by A216, A34, A217, A219, Def5 ; ::_thesis: verum end; len (Sum g1) = i + 1 by A4, A152, MATRLIN:def_6; then r2 = Sum g1 by A7, A155, FINSEQ_2:9; then A233: Sum r2 = Sum (FlattenSeq g1) by POLYNOM1:14; len (FlattenSeq g1) = len (prodTuples (p,q,r,(FlattenSeq g2))) by A189, Def5; then A234: FlattenSeq g1 = prodTuples (p,q,r,(FlattenSeq g2)) by A192, FINSEQ_2:9; len (FlattenSeq f1) = len (prodTuples (p,q,r,(FlattenSeq f2))) by A216, Def5; then FlattenSeq f1 = prodTuples (p,q,r,(FlattenSeq f2)) by A218, FINSEQ_2:9; then A235: FlattenSeq f1 = (FlattenSeq g1) * P by A234, A116, Th15; len (Sum f1) = i + 1 by A1, A123, MATRLIN:def_6; then r1 = Sum f1 by A119, A126, FINSEQ_2:9; then Sum r1 = Sum (FlattenSeq f1) by POLYNOM1:14; hence ((p *' q) *' r) . i = (p *' (q *' r)) . i by A120, A8, A233, A235, RLVECT_2:7; ::_thesis: verum end; hence (p *' q) *' r = p *' (q *' r) by FUNCT_2:63; ::_thesis: verum end; definition let L be non empty commutative Abelian add-associative right_zeroed doubleLoopStr ; let p, q be sequence of L; :: original: *' redefine funcp *' q -> sequence of L; commutativity for p, q being sequence of L holds p *' q = q *' p proof let p, q be sequence of L; ::_thesis: p *' q = q *' p now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_q)_._i_=_(q_*'_p)_._i let i be Element of NAT ; ::_thesis: (p *' q) . i = (q *' p) . i consider r1 being FinSequence of the carrier of L such that A1: len r1 = i + 1 and A2: (p *' q) . i = Sum r1 and A3: for k being Element of NAT st k in dom r1 holds r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9; consider r2 being FinSequence of the carrier of L such that A4: len r2 = i + 1 and A5: (q *' p) . i = Sum r2 and A6: for k being Element of NAT st k in dom r2 holds r2 . k = (q . (k -' 1)) * (p . ((i + 1) -' k)) by Def9; now__::_thesis:_for_k_being_Nat_st_k_in_dom_r1_holds_ r1_._k_=_r2_._(((len_r2)_-_k)_+_1) let k be Nat; ::_thesis: ( k in dom r1 implies r1 . k = r2 . (((len r2) - k) + 1) ) assume A7: k in dom r1 ; ::_thesis: r1 . k = r2 . (((len r2) - k) + 1) then A8: 1 <= k by FINSEQ_3:25; then A9: k - 1 >= 0 by XREAL_1:48; k <= i + 1 by A1, A7, FINSEQ_3:25; then A10: (i + 1) - k >= 0 by XREAL_1:48; then reconsider k1 = ((len r2) - k) + 1 as Element of NAT by A4, INT_1:3; A11: (i + 1) -' k = (((i + 1) - k) + 1) - 1 by A10, XREAL_0:def_2 .= k1 -' 1 by A4, A10, XREAL_0:def_2 ; 1 - k <= 0 by A8, XREAL_1:47; then i + (1 - k) <= i + 0 by XREAL_1:6; then A12: k1 <= i + 1 by A4, XREAL_1:6; then (i + 1) - k1 >= 0 by XREAL_1:48; then A13: (i + 1) -' k1 = (i + 1) - ((i + 1) - (k - 1)) by A4, XREAL_0:def_2 .= k -' 1 by A9, XREAL_0:def_2 ; ((i + 1) - k) + 1 >= 0 + 1 by A10, XREAL_1:6; then A14: k1 in dom r2 by A4, A12, FINSEQ_3:25; thus r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3, A7 .= r2 . (((len r2) - k) + 1) by A6, A14, A13, A11 ; ::_thesis: verum end; then r1 = Rev r2 by A1, A4, FINSEQ_5:def_3; hence (p *' q) . i = (q *' p) . i by A2, A5, Th2; ::_thesis: verum end; hence p *' q = q *' p by FUNCT_2:63; ::_thesis: verum end; end; theorem :: POLYNOM3:34 for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr for p being sequence of L holds p *' (0_. L) = 0_. L proof let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being sequence of L holds p *' (0_. L) = 0_. L let p be sequence of L; ::_thesis: p *' (0_. L) = 0_. L now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(0_._L))_._i_=_(0_._L)_._i let i be Element of NAT ; ::_thesis: (p *' (0_. L)) . i = (0_. L) . i consider r being FinSequence of the carrier of L such that len r = i + 1 and A1: (p *' (0_. L)) . i = Sum r and A2: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by Def9; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r implies r . k = 0. L ) assume k in dom r ; ::_thesis: r . k = 0. L hence r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by A2 .= (p . (k -' 1)) * (0. L) by FUNCOP_1:7 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; hence (p *' (0_. L)) . i = 0. L by A1, Th1 .= (0_. L) . i by FUNCOP_1:7 ; ::_thesis: verum end; hence p *' (0_. L) = 0_. L by FUNCT_2:63; ::_thesis: verum end; theorem Th35: :: POLYNOM3:35 for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr for p being sequence of L holds p *' (1_. L) = p proof let L be non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being sequence of L holds p *' (1_. L) = p let p be sequence of L; ::_thesis: p *' (1_. L) = p now__::_thesis:_for_i_being_Element_of_NAT_holds_(p_*'_(1_._L))_._i_=_p_._i let i be Element of NAT ; ::_thesis: (p *' (1_. L)) . i = p . i consider r being FinSequence of the carrier of L such that A1: len r = i + 1 and A2: (p *' (1_. L)) . i = Sum r and A3: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k)) by Def9; i + 1 in Seg (len r) by A1, FINSEQ_1:4; then A4: i + 1 in dom r by FINSEQ_1:def_3; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Del_(r,(i_+_1)))_holds_ (Del_(r,(i_+_1)))_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom (Del (r,(i + 1))) implies (Del (r,(i + 1))) . k = 0. L ) assume k in dom (Del (r,(i + 1))) ; ::_thesis: (Del (r,(i + 1))) . k = 0. L then A5: k in Seg (len (Del (r,(i + 1)))) by FINSEQ_1:def_3; then k in Seg i by A1, PRE_POLY:12; then A6: k <= i by FINSEQ_1:1; then A7: k < i + 1 by NAT_1:13; A8: (i + 1) - k <> 0 by A6, NAT_1:13; (i + 1) - k >= 0 by A7, XREAL_1:48; then A9: (i + 1) -' k <> 0 by A8, XREAL_0:def_2; 1 <= k by A5, FINSEQ_1:1; then k in Seg (i + 1) by A7, FINSEQ_1:1; then A10: k in dom r by A1, FINSEQ_1:def_3; thus (Del (r,(i + 1))) . k = r . k by A7, FINSEQ_3:110 .= (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k)) by A3, A10 .= (p . (k -' 1)) * (0. L) by A9, Th30 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; then A11: Sum (Del (r,(i + 1))) = 0. L by Th1; r = (Del (r,(i + 1))) ^ <*(r . (i + 1))*> by A1, PRE_POLY:13 .= (Del (r,(i + 1))) ^ <*(r /. (i + 1))*> by A4, PARTFUN1:def_6 ; then A12: Sum r = (Sum (Del (r,(i + 1)))) + (Sum <*(r /. (i + 1))*>) by RLVECT_1:41 .= (Sum (Del (r,(i + 1)))) + (r /. (i + 1)) by RLVECT_1:44 ; r /. (i + 1) = r . (i + 1) by A4, PARTFUN1:def_6 .= (p . ((i + 1) -' 1)) * ((1_. L) . ((i + 1) -' (i + 1))) by A3, A4 .= (p . i) * ((1_. L) . ((i + 1) -' (i + 1))) by NAT_D:34 .= (p . i) * ((1_. L) . 0) by XREAL_1:232 .= (p . i) * (1_ L) by Th30 .= p . i by VECTSP_1:def_4 ; hence (p *' (1_. L)) . i = p . i by A2, A12, A11, RLVECT_1:4; ::_thesis: verum end; hence p *' (1_. L) = p by FUNCT_2:63; ::_thesis: verum end; begin definition let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; func Polynom-Ring L -> non empty strict doubleLoopStr means :Def10: :: POLYNOM3:def 10 ( ( for x being set holds ( x in the carrier of it iff x is Polynomial of L ) ) & ( for x, y being Element of it for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of it for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. it = 0_. L & 1. it = 1_. 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 L ) ) & ( for x, y being Element of b1 for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b1 for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L ) proof A1: 0_. L in { x where x is Polynomial of L : verum } ; then reconsider Ca = { x where x is Polynomial of L : verum } as non empty set ; reconsider Ze = 0_. L as Element of Ca by A1; defpred S1[ set , set , set ] means ex p, q being Polynomial of L st ( p = $1 & q = $2 & $3 = p + q ); A2: for x, y being Element of Ca ex u being Element of Ca st S1[x,y,u] proof let x, y be Element of Ca; ::_thesis: ex u being Element of Ca st S1[x,y,u] x in Ca ; then consider p being Polynomial of L such that A3: x = p ; y in Ca ; then consider q being Polynomial of L such that A4: y = q ; p + q in Ca ; then reconsider u = p + q as Element of Ca ; take u ; ::_thesis: S1[x,y,u] take p ; ::_thesis: ex q being Polynomial of L st ( p = x & q = y & u = p + q ) take q ; ::_thesis: ( p = x & q = y & u = p + q ) thus ( p = x & q = y & u = p + q ) by A3, A4; ::_thesis: verum end; consider Ad being Function of [:Ca,Ca:],Ca such that A5: for x, y being Element of Ca holds S1[x,y,Ad . (x,y)] from BINOP_1:sch_3(A2); 1_. L in { x where x is Polynomial of L : verum } ; then reconsider Un = 1_. L as Element of Ca ; defpred S2[ set , set , set ] means ex p, q being Polynomial of L st ( p = $1 & q = $2 & $3 = p *' q ); A6: for x, y being Element of Ca ex u being Element of Ca st S2[x,y,u] proof let x, y be Element of Ca; ::_thesis: ex u being Element of Ca st S2[x,y,u] x in Ca ; then consider p being Polynomial of L such that A7: x = p ; y in Ca ; then consider q being Polynomial of L such that A8: y = q ; p *' q in Ca ; then reconsider u = p *' q as Element of Ca ; take u ; ::_thesis: S2[x,y,u] take p ; ::_thesis: ex q being Polynomial of L st ( p = x & q = y & u = p *' q ) take q ; ::_thesis: ( p = x & q = y & u = p *' q ) thus ( p = x & q = y & u = p *' q ) by A7, A8; ::_thesis: verum end; consider Mu being Function of [:Ca,Ca:],Ca such that A9: for x, y being Element of Ca holds S2[x,y,Mu . (x,y)] from BINOP_1:sch_3(A6); reconsider P = doubleLoopStr(# Ca,Ad,Mu,Un,Ze #) as non empty strict doubleLoopStr ; take P ; ::_thesis: ( ( for x being set holds ( x in the carrier of P iff x is Polynomial of L ) ) & ( for x, y being Element of P for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of P for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L ) thus for x being set holds ( x in the carrier of P iff x is Polynomial of L ) ::_thesis: ( ( for x, y being Element of P for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of P for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L ) proof let x be set ; ::_thesis: ( x in the carrier of P iff x is Polynomial of L ) thus ( x in the carrier of P implies x is Polynomial of L ) ::_thesis: ( x is Polynomial of L implies x in the carrier of P ) proof assume x in the carrier of P ; ::_thesis: x is Polynomial of L then ex p being Polynomial of L st x = p ; hence x is Polynomial of L ; ::_thesis: verum end; thus ( x is Polynomial of L implies x in the carrier of P ) ; ::_thesis: verum end; thus for x, y being Element of P for p, q being sequence of L st x = p & y = q holds x + y = p + q ::_thesis: ( ( for x, y being Element of P for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L ) proof let x, y be Element of P; ::_thesis: for p, q being sequence of L st x = p & y = q holds x + y = p + q let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x + y = p + q ) assume A10: ( x = p & y = q ) ; ::_thesis: x + y = p + q ex p1, q1 being Polynomial of L st ( p1 = x & q1 = y & Ad . (x,y) = p1 + q1 ) by A5; hence x + y = p + q by A10; ::_thesis: verum end; thus for x, y being Element of P for p, q being sequence of L st x = p & y = q holds x * y = p *' q ::_thesis: ( 0. P = 0_. L & 1. P = 1_. L ) proof let x, y be Element of P; ::_thesis: for p, q being sequence of L st x = p & y = q holds x * y = p *' q let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x * y = p *' q ) assume A11: ( x = p & y = q ) ; ::_thesis: x * y = p *' q ex p1, q1 being Polynomial of L st ( p1 = x & q1 = y & Mu . (x,y) = p1 *' q1 ) by A9; hence x * y = p *' q by A11; ::_thesis: verum end; thus 0. P = 0_. L ; ::_thesis: 1. P = 1_. L thus 1. P = 1_. 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 L ) ) & ( for x, y being Element of b1 for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b1 for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds ( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2 for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b2 for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds b1 = b2 proof let P1, P2 be non empty strict doubleLoopStr ; ::_thesis: ( ( for x being set holds ( x in the carrier of P1 iff x is Polynomial of L ) ) & ( for x, y being Element of P1 for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of P1 for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. P1 = 0_. L & 1. P1 = 1_. L & ( for x being set holds ( x in the carrier of P2 iff x is Polynomial of L ) ) & ( for x, y being Element of P2 for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of P2 for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. P2 = 0_. L & 1. P2 = 1_. L implies P1 = P2 ) assume that A12: for x being set holds ( x in the carrier of P1 iff x is Polynomial of L ) and A13: for x, y being Element of P1 for p, q being sequence of L st x = p & y = q holds x + y = p + q and A14: for x, y being Element of P1 for p, q being sequence of L st x = p & y = q holds x * y = p *' q and A15: ( 0. P1 = 0_. L & 1. P1 = 1_. L ) and A16: for x being set holds ( x in the carrier of P2 iff x is Polynomial of L ) and A17: for x, y being Element of P2 for p, q being sequence of L st x = p & y = q holds x + y = p + q and A18: for x, y being Element of P2 for p, q being sequence of L st x = p & y = q holds x * y = p *' q and A19: ( 0. P2 = 0_. L & 1. P2 = 1_. L ) ; ::_thesis: P1 = P2 A20: now__::_thesis:_for_x_being_set_holds_ (_x_in_the_carrier_of_P1_iff_x_in_the_carrier_of_P2_) let x be set ; ::_thesis: ( x in the carrier of P1 iff x in the carrier of P2 ) ( x in the carrier of P1 iff x is Polynomial of L ) by A12; hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A16; ::_thesis: verum end; then A21: the carrier of P1 = the carrier of P2 by TARSKI:1; A22: now__::_thesis:_for_x_being_Element_of_P1 for_y_being_Element_of_P2_holds_the_multF_of_P1_._(x,y)_=_the_multF_of_P2_._(x,y) let x be Element of P1; ::_thesis: for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y) let y be Element of P2; ::_thesis: the multF of P1 . (x,y) = the multF of P2 . (x,y) reconsider y1 = y as Element of P1 by A20; reconsider x1 = x as Element of P2 by A20; reconsider p = x as sequence of L by A12; reconsider q = y as sequence of L by A16; thus the multF of P1 . (x,y) = x * y1 .= p *' q by A14 .= x1 * y by A18 .= the multF of P2 . (x,y) ; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_P1 for_y_being_Element_of_P2_holds_the_addF_of_P1_._(x,y)_=_the_addF_of_P2_._(x,y) let x be Element of P1; ::_thesis: for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y) let y be Element of P2; ::_thesis: the addF of P1 . (x,y) = the addF of P2 . (x,y) reconsider y1 = y as Element of P1 by A20; reconsider x1 = x as Element of P2 by A20; reconsider p = x as sequence of L by A12; reconsider q = y as sequence of L by A16; thus the addF of P1 . (x,y) = x + y1 .= p + q by A13 .= x1 + y by A17 .= the addF of P2 . (x,y) ; ::_thesis: verum end; then the addF of P1 = the addF of P2 by A21, BINOP_1:2; hence P1 = P2 by A15, A19, A21, A22, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def10 defines Polynom-Ring POLYNOM3:def_10_:_ for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for b2 being non empty strict doubleLoopStr holds ( b2 = Polynom-Ring L iff ( ( for x being set holds ( x in the carrier of b2 iff x is Polynomial of L ) ) & ( for x, y being Element of b2 for p, q being sequence of L st x = p & y = q holds x + y = p + q ) & ( for x, y being Element of b2 for p, q being sequence of L st x = p & y = q holds x * y = p *' q ) & 0. b2 = 0_. L & 1. b2 = 1_. L ) ); registration let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring L -> non empty strict Abelian ; coherence Polynom-Ring L is Abelian proof let p, q be Element of (Polynom-Ring L); :: according to RLVECT_1:def_2 ::_thesis: p + q = q + p reconsider p1 = p, q1 = q as sequence of L by Def10; thus p + q = p1 + q1 by Def10 .= q + p by Def10 ; ::_thesis: verum end; end; registration let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring L -> non empty strict add-associative ; coherence Polynom-Ring L is add-associative proof let p, q, r be Element of (Polynom-Ring L); :: according to RLVECT_1:def_3 ::_thesis: (p + q) + r = p + (q + r) reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def10; A1: q + r = q1 + r1 by Def10; p + q = p1 + q1 by Def10; hence (p + q) + r = (p1 + q1) + r1 by Def10 .= p1 + (q1 + r1) by Th26 .= p + (q + r) by A1, Def10 ; ::_thesis: verum end; cluster Polynom-Ring L -> non empty strict right_zeroed ; coherence Polynom-Ring L is right_zeroed proof let p be Element of (Polynom-Ring L); :: according to RLVECT_1:def_4 ::_thesis: p + (0. (Polynom-Ring L)) = p reconsider p1 = p as sequence of L by Def10; 0. (Polynom-Ring L) = 0_. L by Def10; hence p + (0. (Polynom-Ring L)) = p1 + (0_. L) by Def10 .= p by Th28 ; ::_thesis: verum end; cluster Polynom-Ring L -> non empty right_complementable strict ; coherence Polynom-Ring L is right_complementable proof let p be Element of (Polynom-Ring L); :: according to ALGSTR_0:def_16 ::_thesis: p is right_complementable reconsider p1 = p as Polynomial of L by Def10; reconsider q = - p1 as Element of (Polynom-Ring L) by Def10; take q ; :: according to ALGSTR_0:def_11 ::_thesis: p + q = 0. (Polynom-Ring L) thus p + q = p1 - p1 by Def10 .= 0_. L by Th29 .= 0. (Polynom-Ring L) by Def10 ; ::_thesis: verum end; end; registration let L be non empty right_complementable commutative distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring L -> non empty strict commutative ; coherence Polynom-Ring L is commutative proof let p, q be Element of (Polynom-Ring L); :: according to GROUP_1:def_12 ::_thesis: p * q = q * p reconsider p1 = p, q1 = q as sequence of L by Def10; thus p * q = p1 *' q1 by Def10 .= q * p by Def10 ; ::_thesis: verum end; end; registration let L be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring L -> non empty strict associative ; coherence Polynom-Ring L is associative proof let p, q, r be Element of (Polynom-Ring L); :: according to GROUP_1:def_3 ::_thesis: (p * q) * r = p * (q * r) reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def10; A1: q * r = q1 *' r1 by Def10; p * q = p1 *' q1 by Def10; hence (p * q) * r = (p1 *' q1) *' r1 by Def10 .= p1 *' (q1 *' r1) by Th33 .= p * (q * r) by A1, Def10 ; ::_thesis: verum end; end; Lm2: now__::_thesis:_for_L_being_non_empty_right_complementable_commutative_well-unital_distributive_Abelian_add-associative_right_zeroed_doubleLoopStr_ for_x,_e_being_Element_of_(Polynom-Ring_L)_st_e_=_1._(Polynom-Ring_L)_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds ( x * e = x & e * x = x ) set Pm = Polynom-Ring L; let x, e be Element of (Polynom-Ring L); ::_thesis: ( e = 1. (Polynom-Ring L) implies ( x * e = x & e * x = x ) ) reconsider p = x as Polynomial of L by Def10; assume A1: e = 1. (Polynom-Ring L) ; ::_thesis: ( x * e = x & e * x = x ) A2: 1. (Polynom-Ring L) = 1_. L by Def10; hence x * e = p *' (1_. L) by A1, Def10 .= x by Th35 ; ::_thesis: e * x = x thus e * x = p *' (1_. L) by A1, A2, Def10 .= x by Th35 ; ::_thesis: verum end; registration let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring L -> non empty strict well-unital ; coherence Polynom-Ring L is well-unital proof let x be Element of (Polynom-Ring L); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x ) thus ( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x ) by Lm2; ::_thesis: verum end; end; registration let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring L -> non empty strict distributive ; coherence Polynom-Ring L is distributive proof let p, q, r be Element of (Polynom-Ring L); :: according to VECTSP_1:def_7 ::_thesis: ( p * (q + r) = (p * q) + (p * r) & (q + r) * p = (q * p) + (r * p) ) reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def10; A1: ( p * q = p1 *' q1 & p * r = p1 *' r1 ) by Def10; q + r = q1 + r1 by Def10; hence p * (q + r) = p1 *' (q1 + r1) by Def10 .= (p1 *' q1) + (p1 *' r1) by Th31 .= (p * q) + (p * r) by A1, Def10 ; ::_thesis: (q + r) * p = (q * p) + (r * p) A2: ( q * p = q1 *' p1 & r * p = r1 *' p1 ) by Def10; q + r = q1 + r1 by Def10; hence (q + r) * p = (q1 + r1) *' p1 by Def10 .= (q1 *' p1) + (r1 *' p1) by Th32 .= (q * p) + (r * p) by A2, Def10 ; ::_thesis: verum end; end; theorem :: POLYNOM3:36 for L being non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds 1. (Polynom-Ring L) = 1_. L by Def10;