polynom3.miz

begin

 theorem :: POLYNOM3:1



 Th1: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be FinSequence of the carrier of L st for i be Element of NAT st i in ( dom p) holds (p . i) = ( 0. L) holds ( Sum p) = ( 0. L)

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 let p be FinSequence of the carrier of L;

 assume

 A1: for k be Element of NAT st k in ( dom p) holds (p . k) = ( 0. L);

 now

 let k be Nat;

 assume

 A2: k in ( dom p);



 hence (p /. k) = (p . k) by PARTFUN1:def 6

 .= ( 0. L) by A1, A2;

 end;

 hence thesis by MATRLIN: 11;

 end;

 theorem :: POLYNOM3:2



 Th2: for V be Abelian add-associative right_zeroed non empty addLoopStr holds for p be FinSequence of the carrier of V holds ( Sum p) = ( Sum ( Rev p))

 proof

 let V be Abelian add-associative right_zeroed non empty addLoopStr;

 defpred P[ FinSequence of the carrier of V] means ( Sum $1) = ( Sum ( Rev $1));



 A1: for p be FinSequence of the carrier of V holds for x be Element of V st P[p] holds P[(p ^ <*x*>)]

 proof

 let p be FinSequence of the carrier of V;

 let x be Element of V;

 assume

 A2: ( Sum p) = ( Sum ( Rev p));



 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;

 end;



 A3: P[( <*> the carrier of V)];

 thus for p be FinSequence of the carrier of V holds P[p] from FINSEQ_2:sch 2( A3, A1);

 end;

 theorem :: POLYNOM3:3



 Th3: for p be FinSequence of REAL holds ( Sum p) = ( Sum ( Rev p))

 proof

 defpred P[ FinSequence of REAL ] means ( Sum $1) = ( Sum ( Rev $1));



 A1: for p be FinSequence of REAL holds for x be Element of REAL st P[p] holds P[(p ^ <*x*>)]

 proof

 let p be FinSequence of REAL ;

 let x be Element of REAL ;

 assume

 A2: ( Sum p) = ( Sum ( Rev p));



 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;

 end;



 A3: P[( <*> REAL )];

 thus for p be FinSequence of REAL holds P[p] from FINSEQ_2:sch 2( A3, A1);

 end;

 theorem :: POLYNOM3:4



 Th4: for p be FinSequence of NAT holds for i be Element of NAT st i in ( dom p) holds ( Sum p) >= (p . i)

 proof

 defpred P[ FinSequence of NAT ] means for i be Element of NAT st i in ( dom $1) holds ( Sum $1) >= ($1 . i);



 A1: for p be FinSequence of NAT holds for x be Element of NAT st P[p] holds P[(p ^ <*x*>)]

 proof

 let p be FinSequence of NAT qua set;

 let x be Element of NAT ;

 assume

 A2: for i be Element of NAT st i in ( dom p) holds ( Sum p) >= (p . i);

 let i be Element of NAT ;



 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*>));

 per cases by A5, A4, XBOOLE_0:def 3;

 suppose

 A6: i in ( dom p);

 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 thesis by A6, FINSEQ_1:def 7;

 end;

 suppose i in {(( len p) + 1)};

 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 thesis by RVSUM_1: 74;

 end;

 end;



 A7: P[( <*> NAT ) qua FinSequence of NAT ];

 thus for p be FinSequence of NAT holds P[p] from FINSEQ_2:sch 2( A7, A1);

 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 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 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

 func p ^ q -> Element of ((k + n) -tuples_on D) ;

 coherence

 proof

 (p ^ q) is Tuple of (k + n), D;

 hence thesis by FINSEQ_2: 131;

 end;

 end

 definition

 let D be non empty set;

 let k,n be Nat;

 let p be FinSequence of (k -tuples_on D);

 let q be FinSequence of (n -tuples_on D);

 :: original: ^^

 redefine

 func p ^^ q -> Element of (((k + n) -tuples_on D) * ) ;

 coherence

 proof

 ( rng (p ^^ q)) c= ((k + n) -tuples_on D)

 proof

 let y be object;

 assume y in ( rng (p ^^ q));

 then

 consider x be object such that

 A1: x in ( dom (p ^^ q)) and

 A2: y = ((p ^^ q) . x) by FUNCT_1:def 3;

 reconsider x as set by TARSKI: 1;



 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;

 then y is Tuple of (k + n), D;

 hence thesis by FINSEQ_2: 131;

 end;

 then (p ^^ q) is FinSequence of ((k + n) -tuples_on D) by FINSEQ_1:def 4;

 hence thesis by FINSEQ_1:def 11;

 end;

 end

 scheme :: POLYNOM3:sch1

 SeqOfSeqLambdaD { D() -> non empty set , A() -> Element of NAT , T( Nat) -> Element of NAT , F( set, set) -> Element of D() } :

ex p be FinSequence of (D() * ) st ( len p) = A() & for k be Element of NAT st k in ( Seg A()) holds ( len (p /. k)) = T(k) & for n be Element of NAT st n in ( dom (p /. k)) holds ((p /. k) . n) = F(k,n);

 defpred P[ Nat, FinSequence] means ( len $2) = T($1) & for n be Element of NAT st n in ( dom $2) holds ($2 . n) = F($1,n);



 A1: for k be Nat st k in ( Seg A()) holds ex d be Element of (D() * ) st P[k, d]

 proof

 let k be Nat;

 assume k in ( Seg A());

 deffunc G( Nat) = F(k,$1);

 consider d be FinSequence of D() such that

 A2: ( len d) = T(k) and

 A3: for n be Nat st n in ( dom d) holds (d . n) = G(n) from FINSEQ_2:sch 1;

 reconsider d as Element of (D() * ) by FINSEQ_1:def 11;

 take d;

 thus ( len d) = T(k) by A2;

 let n be Element of NAT ;

 assume n in ( dom d);

 hence thesis by A3;

 end;

 consider p be FinSequence of (D() * ) such that

 A4: ( dom p) = ( Seg A()) and

 A5: for k be Nat st k in ( Seg A()) holds P[k, (p /. k)] from RECDEF_1:sch 17( A1);

 take p;

 thus ( len p) = A() by A4, FINSEQ_1:def 3;

 let k be Element of NAT ;

 assume k in ( Seg A());

 hence thesis by A5;

 end;

 begin

 definition

 let n be Nat;

 let p,q be Element of (n -tuples_on NAT );

 :: POLYNOM3:def1

 pred p < q means ex i be Element of NAT st i in ( Seg n) & (p . i) < (q . i) & for k be Nat st 1 <= k & k < i holds (p . k) = (q . k);

 asymmetry

 proof

 let p,q be Element of (n -tuples_on NAT );

 given i be Element of NAT such that

 A1: i in ( Seg n) and

 A2: (p . i) < (q . i) and

 A3: for k be Nat st 1 <= k & k < i holds (p . k) = (q . k);



 A4: 1 <= i by A1, FINSEQ_1: 1;

 given j be Element of NAT such that

 A5: j in ( Seg n) and

 A6: (q . j) < (p . j) and

 A7: for k be Nat st 1 <= k & k < j holds (q . k) = (p . k);



 A8: 1 <= j by A5, FINSEQ_1: 1;

 per cases by XXREAL_0: 1;

 suppose i < j;

 hence contradiction by A2, A7, A4;

 end;

 suppose j < i;

 hence contradiction by A3, A6, A8;

 end;

 suppose i = j;

 hence contradiction by A2, A6;

 end;

 end;

 end

 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 );

 :: POLYNOM3:def2

 pred p <= q means p < q or p = q;

 reflexivity ;

 end

 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 :: POLYNOM3:5



 Th5: for n be Element of NAT holds for p,q,r be 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 ;

 let p,q,r be Element of (n -tuples_on NAT );

 thus

 A1: p < q & q < r implies p < r

 proof

 assume that

 A2: p < q and

 A3: q < r;

 consider i be Element of NAT such that

 A4: i in ( Seg n) and

 A5: (p . i) < (q . i) and

 A6: for k be Nat st 1 <= k & k < i holds (p . k) = (q . k) by A2;

 consider j be Element of NAT such that

 A7: j in ( Seg n) and

 A8: (q . j) < (r . j) and

 A9: for k be Nat st 1 <= k & k < j holds (q . k) = (r . k) by A3;

 reconsider t = ( min (i,j)) as Element of NAT ;

 take t;

 thus t in ( Seg n) by A4, A7, XXREAL_0: 15;

 now

 per cases by XXREAL_0: 1;

 suppose

 A10: i < j;



 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;

 end;

 suppose

 A12: i > j;



 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;

 end;

 suppose i = j;

 hence (p . t) < (r . t) by A5, A8, XXREAL_0: 2;

 end;

 end;

 hence (p . t) < (r . t);

 let k be Nat;

 assume that

 A14: 1 <= k and

 A15: k < t;

 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;

 end;

 assume

 A17: p < q & q <= r or p <= q & q < r or p <= q & q <= r;

 per cases by A17;

 suppose

 A18: p < q & q <= r;

 thus thesis by A1, A18;

 end;

 suppose

 A19: p <= q & q < r;

 thus thesis by A1, A19;

 end;

 suppose p <= q & q <= r;

 hence thesis by A1;

 end;

 end;

 theorem :: POLYNOM3:6



 Th6: for n be Nat holds for p,q be Element of (n -tuples_on NAT ) holds p <> q implies ex i be Element of NAT st i in ( Seg n) & (p . i) <> (q . i) & for k be Nat st 1 <= k & k q implies ex i be Element of NAT st i in ( Seg $1) & (p . i) <> (q . i) & for k be Nat st 1 <= k & k q implies ex i be Element of NAT st i in ( Seg n) & (p . i) <> (q . i) & for k be Nat st 1 <= k & k ) by FINSEQ_2: 117;

 assume

 A4: p <> q;

 consider t2 be Element of (n -tuples_on NAT ), d2 be 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;

 per cases ;

 suppose t1 <> t2;

 then

 consider i be Element of NAT such that

 A8: i in ( Seg n) and

 A9: (t1 . i) <> (t2 . i) and

 A10: for k be Nat st 1 <= k & k < i holds (t1 . k) = (t2 . k) by A2;

 take i;

 thus i in ( Seg (n + 1)) by A8, FINSEQ_2: 8;

 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;

 let k be Nat;

 assume that

 A12: 1 <= k and

 A13: k < i;

 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;

 end;

 suppose

 A17: t1 = t2;

 take i = (n + 1);

 thus i in ( Seg (n + 1)) by FINSEQ_1: 4;

 (p . i) = d1 by A3, FINSEQ_2: 116;

 hence (p . i) <> (q . i) by A3, A5, A4, A17, FINSEQ_2: 116;

 let k be Nat;

 assume that

 A18: 1 <= k and

 A19: k < i;



 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;

 end;

 end;



 A22: P[ 0 ];

 thus for n be Nat holds P[n] from NAT_1:sch 2( A22, A1);

 end;

 theorem :: POLYNOM3:7



 Th7: for n be Element of NAT holds for p,q be Element of (n -tuples_on NAT ) holds p <= q or p > q

 proof

 let n be Element of NAT ;

 let p,q be Element of (n -tuples_on NAT );

 assume

 A1: not p <= q;

 then

 consider i be Element of NAT such that

 A2: i in ( Seg n) and

 A3: (p . i) <> (q . i) and

 A4: for k be Nat st 1 <= k & k = (q . i) by A2, A4;

 hence (q . i) < (p . i) by A3, XXREAL_0: 1;

 thus thesis by A4;

 end;

 definition

 let n be Element of NAT ;

 :: POLYNOM3:def3

 func TuplesOrder n -> Order of (n -tuples_on NAT ) means

 : Def3: for p,q be Element of (n -tuples_on NAT ) holds [p, q] in it iff p <= q;

 existence

 proof

 defpred P[ Element of (n -tuples_on NAT ), Element of (n -tuples_on NAT )] means $1 <= $2;

 consider R be Relation of (n -tuples_on NAT ), (n -tuples_on NAT ) such that

 A1: for x,y be Element of (n -tuples_on NAT ) holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;



 A2: R is_transitive_in (n -tuples_on NAT )

 proof

 let x,y,z be object;

 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;

 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 thesis by A1;

 end;



 A5: R is_reflexive_in (n -tuples_on NAT ) by A1;

 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 object;

 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;

 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;

 y1 <= x1 by A1, A9;

 hence thesis by A10;

 end;

 then

 reconsider 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;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let T1,T2 be Order of (n -tuples_on NAT ) such that

 A11: for p,q be Element of (n -tuples_on NAT ) holds [p, q] in T1 iff p <= q and

 A12: for p,q be Element of (n -tuples_on NAT ) holds [p, q] in T2 iff p <= q;

 let x,y be object;

 thus [x, y] in T1 implies [x, y] in T2

 proof

 assume

 A13: [x, y] in T1;

 then

 consider p,q be object 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, q as Element of (n -tuples_on NAT ) by A15;

 p <= q by A11, A13, A14;

 hence thesis by A12, A14;

 end;

 assume

 A16: [x, y] in T2;

 then

 consider p,q be object 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, q as Element of (n -tuples_on NAT ) by A18;

 p <= q by A12, A16, A17;

 hence thesis by A11, A17;

 end;

 end

 registration

 let n be Element of NAT ;

 cluster ( TuplesOrder n) -> being_linear-order;

 coherence

 proof

 now

 let x,y be object;

 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);

 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;

 hence [y, x] in ( TuplesOrder n) by Def3;

 end;

 then ( field ( TuplesOrder n)) = (n -tuples_on NAT ) & ( TuplesOrder n) is_connected_in (n -tuples_on NAT ) by ORDERS_1: 15;

 then ( TuplesOrder n) is connected;

 hence thesis by ORDERS_1:def 6;

 end;

 end

 begin

 definition

 let i be non zero Element of NAT ;

 let n be Element of NAT ;

 :: POLYNOM3:def4

 func Decomp (n,i) -> FinSequence of (i -tuples_on NAT ) means

 : Def4: ex A be finite Subset of (i -tuples_on NAT ) st it = ( SgmX (( TuplesOrder i),A)) & for p be Element of (i -tuples_on NAT ) holds p in A iff ( Sum p) = n;

 existence

 proof

 reconsider n1 = (n + 1) as non empty set;

 defpred P[ Element of (i -tuples_on NAT )] means ( Sum $1) = n;

 consider A be Subset of (i -tuples_on NAT ) such that

 A1: for p be Element of (i -tuples_on NAT ) holds p in A iff P[p] from SUBSET_1:sch 3;



 A2: A c= (i -tuples_on (n + 1))

 proof

 let x be object;

 assume

 A3: x in A;

 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 object;

 assume that

 A5: y in ( rng p) and

 A6: not y in (n + 1);

 ( 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 be Nat : t < (n + 1) } by A6, AXIOMS: 4;

 then

 A7: k >= (n + 1);

 ex j be 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;

 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 thesis;

 end;

 reconsider A as finite Subset of (i -tuples_on NAT ) by A2;

 take ( SgmX (( TuplesOrder i),A));

 thus thesis by A1;

 end;

 uniqueness

 proof

 let p1,p2 be FinSequence of (i -tuples_on NAT );

 given A1 be finite Subset of (i -tuples_on NAT ) such that

 A8: p1 = ( SgmX (( TuplesOrder i),A1)) and

 A9: for p be Element of (i -tuples_on NAT ) holds p in A1 iff ( Sum p) = n;

 given A2 be finite Subset of (i -tuples_on NAT ) such that

 A10: p2 = ( SgmX (( TuplesOrder i),A2)) and

 A11: for p be Element of (i -tuples_on NAT ) holds p in A2 iff ( Sum p) = n;

 now

 let x be object;

 thus x in A1 implies x in A2

 proof

 assume

 A12: x in A1;

 then

 reconsider p = x as Element of (i -tuples_on NAT );

 ( Sum p) = n by A9, A12;

 hence thesis by A11;

 end;

 assume

 A13: x in A2;

 then

 reconsider p = x as Element of (i -tuples_on NAT );

 ( Sum p) = n by A11, A13;

 hence x in A1 by A9;

 end;

 hence thesis by A8, A10, TARSKI: 2;

 end;

 end

 registration

 let i be non zero Element of NAT ;

 let n be Element of NAT ;

 cluster ( Decomp (n,i)) -> non empty one-to-one FinSequence-yielding;

 coherence

 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 be finite Subset of (i -tuples_on NAT ) such that

 A1: ( Decomp (n,i)) = ( SgmX (( TuplesOrder i),A)) and

 A2: for p be 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 as non empty finite Subset of (i -tuples_on NAT ) by A2;

 ( SgmX (( TuplesOrder i),A)) is non empty finite;

 hence thesis by A1;

 end;

 end

 theorem :: POLYNOM3:8



 Th8: for n be Element of NAT holds ( len ( Decomp (n,1))) = 1

 proof

 let n be Element of NAT ;

 consider A be finite Subset of (1 -tuples_on NAT ) such that

 A1: ( Decomp (n,1)) = ( SgmX (( TuplesOrder 1),A)) and

 A2: for p be Element of (1 -tuples_on NAT ) holds p in A iff ( Sum p) = n by Def4;



 A3: A = { <*n*>}

 proof

 thus A c= { <*n*>}

 proof

 let y be object;

 assume

 A4: y in A;

 then

 reconsider p = y as Element of (1 -tuples_on NAT );



 A5: ( Sum p) = n by A2, A4;

 consider k be Element of NAT such that

 A6: p = <*k*> by FINSEQ_2: 97;

 ( Sum p) = k by A6, RVSUM_1: 73;

 hence thesis by A5, A6, TARSKI:def 1;

 end;

 let y be object;

 assume y in { <*n*>};

 then

 A7: y = <*n*> by TARSKI:def 1;

 ( Sum <*n*>) = n by RVSUM_1: 73;

 hence y in A by A2, A7;

 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;

 end;

 theorem :: POLYNOM3:9



 Th9: for n be Element of NAT holds ( len ( Decomp (n,2))) = (n + 1)

 proof

 let n be Element of NAT ;

 deffunc F( Nat) = <*$1, (n -' $1)*>;

 consider q be FinSequence such that

 A1: ( len q) = n and

 A2: for k be Nat st k in ( dom q) holds (q . k) = F(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 q1) = (n + 1) by A1, FINSEQ_2: 16;

 then

 A6: ( dom q1) = ( Seg (n + 1)) by FINSEQ_1:def 3;

 now

 let x1,x2 be object;

 assume that

 A7: x1 in ( dom q1) and

 A8: x2 in ( dom q1) and

 A9: (q1 . x1) = (q1 . 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

 per cases by A11, A10, TARSKI:def 1;

 suppose

 A12: x1 in ( Seg n) & x2 in ( Seg n);

 then

 A13: (q1 . k1) = (q . k1) & (q1 . 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;

 end;

 suppose

 A14: x1 in ( Seg n) & x2 = (n + 1);

 then

 A15: (q1 . k2) = <* 0 , n*> by A1, FINSEQ_1: 42;

 (q1 . 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;

 end;

 suppose

 A16: x1 = (n + 1) & x2 in ( Seg n);

 then

 A17: (q1 . k1) = <* 0 , n*> by A1, FINSEQ_1: 42;

 (q1 . 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;

 end;

 suppose x1 = (n + 1) & x2 = (n + 1);

 hence x1 = x2;

 end;

 end;

 hence x1 = x2;

 end;

 then q1 is one-to-one by FUNCT_1:def 4;

 then

 A18: ( card ( rng q1)) = (n + 1) by A5, FINSEQ_4: 62;



 A19: ( rng q) c= ( rng q1) by FINSEQ_1: 29;



 A20: ( rng q1) = { <*i, (n -' i)*> where i be Element of NAT : i <= n }

 proof

 thus ( rng q1) c= { <*i, (n -' i)*> where i be Element of NAT : i <= n }

 proof

 let x be object;

 assume x in ( rng q1);

 then

 consider j be Nat such that

 A21: j in ( dom q1) and

 A22: (q1 . j) = x by FINSEQ_2: 10;

 reconsider 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

 per cases by A23, TARSKI:def 1;

 suppose

 A24: j in ( Seg n);

 then

 A25: (q1 . j) = (q . j) by A3, FINSEQ_1:def 7;

 (q . j) = <*j, (n -' j)*> & j <= n by A2, A4, A24, FINSEQ_1: 1;

 hence thesis by A22, A25;

 end;

 suppose j = (n + 1);



 then (q1 . j) = <* 0 , n*> by A1, FINSEQ_1: 42

 .= <* 0 , (n -' 0 )*> by NAT_D: 40;

 hence thesis by A22;

 end;

 end;

 hence thesis;

 end;

 let x be object;

 assume x in { <*i, (n -' i)*> where i be Element of NAT : i <= n };

 then

 consider i be Element of NAT such that

 A26: x = <*i, (n -' i)*> and

 A27: i <= n;



 A28: i = 0 or i >= ( 0 qua Nat + 1) by NAT_1: 13;

 now

 per cases by A27, A28, FINSEQ_1: 1;

 suppose

 A29: i = 0 ;



 A30: (n + 1) in ( dom q1) by A6, FINSEQ_1: 4;

 (q1 . (n + 1)) = <* 0 , n*> by A1, FINSEQ_1: 42

 .= x by A26, A29, NAT_D: 40;

 hence thesis by A30, FUNCT_1:def 3;

 end;

 suppose

 A31: i in ( Seg n);

 then (q . i) = x by A2, A4, A26;

 then x in ( rng q) by A3, A31, FUNCT_1:def 3;

 hence thesis by A19;

 end;

 end;

 hence thesis;

 end;

 consider A be finite Subset of (2 -tuples_on NAT ) such that

 A32: ( Decomp (n,2)) = ( SgmX (( TuplesOrder 2),A)) and

 A33: for p be Element of (2 -tuples_on NAT ) holds p in A iff ( Sum p) = n by Def4;



 A34: A = { <*i, (n -' i)*> where i be Element of NAT : i <= n }

 proof

 thus A c= { <*i, (n -' i)*> where i be Element of NAT : i <= n }

 proof

 let x be object;

 assume

 A35: x in A;

 then

 reconsider p = x as Element of (2 -tuples_on NAT );

 consider d1,d2 be 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 thesis by A36, A38;

 end;

 let x be object;

 assume x in { <*i, (n -' i)*> where i be Element of NAT : i <= n };

 then

 consider i be 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 thesis by A33, A39;

 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 thesis by A32, A34, A20, A18, ORDERS_1: 38, PRE_POLY: 11;

 end;

 theorem :: POLYNOM3:10

 for n be Element of NAT holds ( Decomp (n,1)) = <* <*n*>*>

 proof

 let n be Element of NAT ;

 consider A be finite Subset of (1 -tuples_on NAT ) such that

 A1: ( Decomp (n,1)) = ( SgmX (( TuplesOrder 1),A)) and

 A2: for p be Element of (1 -tuples_on NAT ) holds p in A iff ( Sum p) = n by Def4;



 A3: A = { <*n*>}

 proof

 thus A c= { <*n*>}

 proof

 let y be object;

 assume

 A4: y in A;

 then

 reconsider p = y as Element of (1 -tuples_on NAT );



 A5: ( Sum p) = n by A2, A4;

 consider k be Element of NAT such that

 A6: p = <*k*> by FINSEQ_2: 97;

 ( Sum p) = k by A6, RVSUM_1: 73;

 hence thesis by A5, A6, TARSKI:def 1;

 end;

 let y be object;

 assume y in { <*n*>};

 then

 A7: y = <*n*> by TARSKI:def 1;

 ( Sum <*n*>) = n by RVSUM_1: 73;

 hence thesis by A2, A7;

 end;

 ( len ( Decomp (n,1))) = 1 by Th8;



 then

 A8: ( 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 thesis by A8, FUNCT_1: 7;

 end;

 theorem :: POLYNOM3:11



 Th11: for i,j,n,k1,k2 be 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 ;

 assume that

 A1: (( Decomp (n,2)) . i) = <*k1, (n -' k1)*> and

 A2: (( Decomp (n,2)) . j) = <*k2, (n -' 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 be finite Subset of (2 -tuples_on NAT ) such that

 A5: ( Decomp (n,2)) = ( SgmX (( TuplesOrder 2),A)) and for p be 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

 proof

 assume

 A9: i < j;

 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;

 then

 consider t be Element of NAT such that

 A11: t in ( Seg 2) and

 A12: ( <*k1, (n -' k1)*> . t) < ( <*k2, (n -' k2)*> . t) and

 A13: for k be Nat st 1 <= k & k < t holds ( <*k1, (n -' k1)*> . k) = ( <*k2, (n -' k2)*> . k);

 per cases by A11, FINSEQ_1: 2, TARSKI:def 2;

 suppose

 A14: t = 1;

 then ( <*k1, (n -' k1)*> . t) = k1 by FINSEQ_1: 44;

 hence thesis by A12, A14, FINSEQ_1: 44;

 end;

 suppose t = 2;

 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 thesis by A12;

 end;

 end;

 assume

 A15: k1 < k2;



 A16: for k be 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;

 assume

 A19: i >= j;

 per cases by A19, XXREAL_0: 1;

 suppose i = j;

 hence contradiction by A1, A2, A15, A17, FINSEQ_1: 44;

 end;

 suppose j < i;

 then [ <*k2, (n -' k2)*>, <*k1, (n -' k1)*>] in ( TuplesOrder 2) by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def 2;

 then

 A20: <*k2, (n -' k2)*> <= <*k1, (n -' k1)*> by Def3;

 thus contradiction by A18, A20;

 end;

 end;

 theorem :: POLYNOM3:12



 Th12: for i,n,k1,k2 be 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 ;

 assume that

 A1: (( Decomp (n,2)) . i) = <*k1, (n -' k1)*> and

 A2: (( Decomp (n,2)) . (i + 1)) = <*k2, (n -' k2)*>;

 assume

 A3: k2 <> (k1 + 1);

 (i + 0 qua Nat) < (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 be finite Subset of (2 -tuples_on NAT ) such that

 A6: ( Decomp (n,2)) = ( SgmX (( TuplesOrder 2),A)) and

 A7: for p be 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;

 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;

 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 be 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 as Element of NAT by ORDINAL1:def 12;

 (k1 + 0 qua Nat) < (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;

 end;

 theorem :: POLYNOM3:13



 Th13: for n be Element of NAT holds (( Decomp (n,2)) . 1) = <* 0 , n*>

 proof

 let n be Element of NAT ;

 consider A be finite Subset of (2 -tuples_on NAT ) such that

 A1: ( Decomp (n,2)) = ( SgmX (( TuplesOrder 2),A)) and

 A2: for p be Element of (2 -tuples_on NAT ) holds p in A iff ( Sum p) = n by Def4;

 A3:

 now

 let y be Element of (2 -tuples_on NAT );

 consider d1,d2 be Element of NAT such that

 A4: y = <*d1, d2*> by FINSEQ_2: 100;

 assume y in A;

 then ( Sum <*d1, d2*>) = n by A2, A4;

 then

 A5: (d1 + d2) = n by RVSUM_1: 77;

 now

 per cases ;

 suppose d1 = 0 ;

 hence <* 0 , n*> <= <*d1, d2*> by A5;

 end;

 suppose d1 > 0 ;

 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 be Nat st 1 <= k & k < 1 holds ( <* 0 , n*> . k) = ( <*d1, d2*> . k) by FINSEQ_1: 1;

 then <* 0 , n*> < <*d1, d2*> by A6;

 hence <* 0 , n*> <= <*d1, d2*>;

 end;

 end;

 hence [ <* 0 , n*>, y] in ( TuplesOrder 2) by A4, Def3;

 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 qua Nat + 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 thesis by A1, A7, PARTFUN1:def 6;

 end;

 theorem :: POLYNOM3:14



 Th14: for n,i be 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 ;

 defpred P[ Nat] means $1 <= (n + 1) implies (( Decomp (n,2)) . $1) = <*($1 -' 1), ((n + 1) -' $1)*>;

 assume i in ( Seg (n + 1));

 then

 A1: 1 <= i & i <= (n + 1) by FINSEQ_1: 1;

 consider A be finite Subset of (2 -tuples_on NAT ) such that

 A2: ( Decomp (n,2)) = ( SgmX (( TuplesOrder 2),A)) and

 A3: for p be Element of (2 -tuples_on NAT ) holds p in A iff ( Sum p) = n by Def4;



 A4: for j be non zero Nat st P[j] holds P[(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 zero Nat;

 assume that

 A6: j <= (n + 1) implies (( Decomp (n,2)) . j) = <*(j -' 1), ((n + 1) -' j)*> and

 A7: (j + 1) <= (n + 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 zero 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 be 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 thesis by A12, A14, A9, NAT_D: 34;

 end;



 A17: P[1]

 proof

 assume 1 <= (n + 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;

 end;

 for j be non zero Nat holds P[j] from NAT_1:sch 10( A17, A4);

 hence thesis by A1;

 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 );

 :: POLYNOM3:def5

 func prodTuples (p,q,r,t) -> Element of (the carrier of L * ) means

 : Def5: ( len it ) = ( len t) & for k be Element of NAT st k in ( dom t) holds (it . k) = (((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)));

 existence

 proof

 deffunc F( Nat) = (((p . ((t /. $1) /. 1)) * (q . ((t /. $1) /. 2))) * (r . ((t /. $1) /. 3)));

 consider p1 be FinSequence of the carrier of L such that

 A1: ( len p1) = ( len t) and

 A2: for k be Nat st k in ( dom p1) holds (p1 . k) = F(k) from FINSEQ_2:sch 1;



 A3: ( dom p1) = ( Seg ( len t)) by A1, FINSEQ_1:def 3;

 reconsider p1 as Element of (the carrier of L * ) by FINSEQ_1:def 11;

 take p1;

 thus ( len p1) = ( len t) by A1;

 let k be Element of NAT ;

 assume k in ( dom t);

 then k in ( Seg ( len t)) by FINSEQ_1:def 3;

 hence thesis by A2, A3;

 end;

 uniqueness

 proof

 let p1,p2 be Element of (the carrier of L * ) such that

 A4: ( len p1) = ( len t) and

 A5: for k be 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 be Element of NAT st k in ( dom t) holds (p2 . k) = (((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)));



 A8: ( dom p1) = ( Seg ( len t)) by A4, FINSEQ_1:def 3;

 now

 let i be Nat;

 assume i in ( dom p1);

 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;

 end;

 hence thesis by A4, A6, FINSEQ_2: 9;

 end;

 end

 theorem :: POLYNOM3:15



 Th15: for L be non empty multMagma holds for p,q,r be sequence of L holds for t be FinSequence of (3 -tuples_on NAT ) holds for P be Permutation of ( dom t) holds for t1 be 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;

 let p,q,r be sequence of L;

 let t be FinSequence of (3 -tuples_on NAT );

 let P be Permutation of ( dom t);

 let t1 be FinSequence of (3 -tuples_on NAT );



 A1: ( rng P) = ( dom t) by FUNCT_2:def 3;

 assume

 A2: t1 = (t * P);

 then

 A3: ( dom P) = ( dom t1) by A1, RELAT_1: 27;

 A4:

 now

 let x be object;

 assume

 A5: x in ( dom t1);

 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;

 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 thesis by A8, A9, A4, FUNCT_1: 2;

 end;

 theorem :: POLYNOM3:16



 Th16: for D be set, f be FinSequence of (D * ), i be Nat holds ( Card (f | i)) = (( Card f) | i)

 proof

 let D be set;

 let f be FinSequence of (D * );

 let i be Nat;



 A1: (f | i) = (f | ( Seg i)) by FINSEQ_1:def 15;

 reconsider k = ( min (i,( len f))) as Nat by TARSKI: 1;

 ( 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



 A7: ( len f) = ( len ( Card f)) by A4, FINSEQ_3: 29;

 let j be Nat;

 assume

 A8: j in ( dom ( Card (f | i)));

 per cases ;

 suppose

 A9: i <= ( len f);



 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 qua set;



 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;

 end;

 suppose

 A16: i > ( len f);

 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;

 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 thesis by A2, A6, FINSEQ_2: 9;

 end;

 ::$Canceled

 theorem :: POLYNOM3:18



 Th17: for p be FinSequence of NAT holds for i,j be Nat st i <= j holds ( Sum (p | i)) <= ( Sum (p | j))

 proof

 let p be FinSequence of NAT ;

 let i,j be Nat;

 assume

 A1: i <= j;

 then

 consider k be Nat such that

 A2: j = (i + k) by NAT_1: 10;

 reconsider k as Element of NAT by ORDINAL1:def 12;

 per cases ;

 suppose

 A3: j <= ( len p);

 then

 A4: ( len (p | j)) = (i + k) by A2, FINSEQ_1: 59;

 then

 consider q,r be 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

 reconsider p1 = p as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

 let n be Nat;

 assume

 A10: n in ( dom (p | i));

 then

 A11: ((p | 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: ((p | j) /. n) = (p /. n) by A10, A13, FINSEQ_4: 70;



 thus ((p | i) . n) = ((p | 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;

 end;



 A15: (( Sum q) + ( Sum r)) >= (( Sum q) + 0 qua Nat) by XREAL_1: 6;

 ( Sum (p | j)) = (( Sum q) + ( Sum r)) by A6, RVSUM_1: 75;

 hence thesis by A7, A5, A9, A15, FINSEQ_2: 9;

 end;

 suppose j > ( len p);

 then

 A16: (p | j) = p by FINSEQ_1: 58;

 now

 per cases ;

 suppose i >= ( len p);

 hence thesis by A16, FINSEQ_1: 58;

 end;

 suppose

 A17: i < ( len p);

 then

 consider t be Nat such that

 A18: ( len p) = (i + t) by NAT_1: 10;

 consider q,r be 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



 A24: ( Seg i) = ( dom q) by A19, FINSEQ_1:def 3;

 let n be Nat;



 A25: ( dom (p | i)) c= ( dom p) by FINSEQ_5: 18;

 assume

 A26: n in ( dom (p | i));

 then

 A27: ((p | i) /. n) = (p /. n) by FINSEQ_4: 70;



 thus ((p | i) . n) = ((p | 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;

 end;



 A28: (( Sum q) + ( Sum r)) >= (( Sum q) + 0 qua Nat) by XREAL_1: 6;

 ( Sum p) = (( Sum q) + ( Sum r)) by A20, RVSUM_1: 75;

 hence thesis by A16, A19, A21, A23, A28, FINSEQ_2: 9;

 end;

 end;

 hence thesis;

 end;

 end;

 ::$Canceled

 theorem :: POLYNOM3:20



 Th19: for p be FinSequence of REAL holds for i be 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 ;

 let i be Element of NAT ;

 assume i < ( len p);

 then (p | (i + 1)) = ((p | i) ^ <*(p . (i + 1))*>) by FINSEQ_5: 83;

 hence thesis by RVSUM_1: 74;

 end;

 theorem :: POLYNOM3:21



 Th20: for p be FinSequence of NAT holds for i,j,k1,k2 be 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 ;

 let i,j,k1,k2 be Element of NAT ;

 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;



 A9: i <> j by A7, A8, XCMPLX_1: 2;

 reconsider p1 = p as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;



 A10: (( Sum (p | i)) + (p . (i + 1))) >= (( Sum (p | i)) + k1) by A5, XREAL_1: 6;



 A11: (( Sum (p | j)) + (p . (j + 1))) >= (( Sum (p | j)) + k2) by A6, XREAL_1: 6;

 per cases ;

 suppose i < j;

 then (i + 1) <= j by NAT_1: 13;

 then ( Sum (p | j)) >= ( Sum (p | (i + 1))) by Th17;

 then ( Sum (p | j)) >= (( Sum (p1 | i)) + (p . (i + 1))) by A1, Th19;

 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;

 end;

 suppose i >= j;

 then j = ( Sum (p | (j + 1))) by Th17;

 then ( Sum (p | i)) >= (( Sum (p1 | j)) + (p . (j + 1))) by A2, Th19;

 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;

 end;

 end;

 theorem :: POLYNOM3:22



 Th21: for D1,D2 be set holds for f1 be FinSequence of (D1 * ) holds for f2 be FinSequence of (D2 * ) holds for i1,i2,j1,j2 be 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;

 let f1 be FinSequence of (D1 * );

 let f2 be FinSequence of (D2 * );

 let i1,i2,j1,j2 be Element of NAT ;

 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);



 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, Th20;

 then (i1 - 1) = (i2 -' 1) by A8, XREAL_0:def 2;

 then (i1 - 1) = (i2 - 1) by A11, XREAL_0:def 2;

 hence thesis by A5, A14, A6, A9, A15, Th20;

 end;

 begin

 definition

 let L be non empty ZeroStr;

 mode Polynomial of L is AlgSequence of L;

 end

 theorem :: POLYNOM3:23

 for L be non empty ZeroStr holds for p be Polynomial of L holds for n be Element of NAT holds n >= ( len p) iff n is_at_least_length_of p by ALGSEQ_1: 8, XXREAL_0: 2, ALGSEQ_1:def 3;

 scheme :: POLYNOM3:sch2

 PolynomialLambdaF { R() -> non empty addLoopStr , A() -> Element of NAT , F( Element of NAT ) -> Element of R() } :

ex p be Polynomial of R() st ( len p) <= A() & for n be Element of NAT st n < A() holds (p . n) = F(n);

 defpred P[ Element of NAT , Element of R()] means $1 < A() & $2 = F($1) or $1 >= A() & $2 = ( 0. R());



 A1: for x be Element of NAT holds ex y be Element of R() st P[x, y]

 proof

 let x be Element of NAT ;

 x < A() implies x < A() & F(x) = F(x);

 hence thesis;

 end;

 ex f be sequence of the carrier of R() st for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

 then

 consider f be sequence of the carrier of R() such that

 A2: for x be Element of NAT holds x < A() & (f . x) = F(x) or x >= A() & (f . x) = ( 0. R());

 ex n be Nat st for i be Nat st i >= n holds (f . i) = ( 0. R())

 proof

 take A();

 let i be Nat;

 i in NAT by ORDINAL1:def 12;

 hence thesis by A2;

 end;

 then

 reconsider f as AlgSequence of R() by ALGSEQ_1:def 1;

 take f;

 now

 let i be Nat;

 i in NAT by ORDINAL1:def 12;

 hence i >= A() implies (f . i) = ( 0. R()) by A2;

 end;

 then A() is_at_least_length_of f;

 hence thesis by A2, ALGSEQ_1:def 3;

 end;

 registration

 let L be right_zeroed non empty addLoopStr;

 let p,q be Polynomial of L;

 cluster (p + q) -> finite-Support;

 coherence

 proof

 take s = (( len p) + ( len q));

 let i be Nat;

 assume

 A1: i >= s;

 (( 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;



 thus ((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;

 end;

 end

 theorem :: POLYNOM3:24

 for L be right_zeroed non empty addLoopStr holds for p,q be Polynomial of L holds for n be Element of NAT holds (n is_at_least_length_of p & n is_at_least_length_of q) implies n is_at_least_length_of (p + q)

 proof

 let L be right_zeroed non empty addLoopStr;

 let p,q be Polynomial of L;

 let n be Element of NAT ;

 assume

 A1: n is_at_least_length_of p & n is_at_least_length_of q;

 let i be Nat;

 assume i >= n;

 then

 A2: (p . i) = ( 0. L) & (q . i) = ( 0. L) by A1;



 thus ((p + q) . i) = (( 0. L) + ( 0. L)) by A2, NORMSP_1:def 2

 .= ( 0. L) by RLVECT_1:def 4;

 end;

 definition

 let L be Abelian non empty addLoopStr;

 let p,q be sequence of L;

 :: original: +

 redefine

 func p + q;

 commutativity

 proof

 let p,q be sequence of L;

 let n be Element of NAT ;



 thus ((p + q) . n) = ((p . n) + (q . n)) by NORMSP_1:def 2

 .= ((q + p) . n) by NORMSP_1:def 2;

 end;

 end

 ::$Canceled

 theorem :: POLYNOM3:26



 Th24: for L be add-associative non empty addLoopStr holds for p,q,r be sequence of L holds ((p + q) + r) = (p + (q + r))

 proof

 let L be add-associative non empty addLoopStr;

 let p,q,r be sequence of L;

 now

 let n be Element of NAT ;



 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;

 end;

 hence thesis;

 end;

 registration

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 let p be Polynomial of L;

 cluster ( - p) -> finite-Support;

 coherence

 proof

 take s = ( len p);

 let i be Nat;

 assume

 A1: i >= s;



 thus (( - p) . i) = ( - (p . i)) by BHSP_1: 44

 .= ( - ( 0. L)) by A1, ALGSEQ_1: 8

 .= ( 0. L) by RLVECT_1: 12;

 end;

 end



 Lm1: for L be non empty addLoopStr holds for p,q be sequence of L holds (p - q) = (p + ( - q))

 proof

 let L be non empty addLoopStr;

 let p,q be sequence of L;

 let n be Element of NAT ;



 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;

 end;

 definition

 let L be non empty addLoopStr;

 let p,q be sequence of L;

 :: original: -

 redefine

 :: POLYNOM3:def6

 func p - q equals (p + ( - q));

 compatibility by Lm1;

 end

 registration

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 let p,q be Polynomial of L;

 cluster (p - q) -> finite-Support;

 coherence ;

 end

 theorem :: POLYNOM3:27

 for L be non empty addLoopStr holds for p,q be sequence of L holds for n be Element of NAT holds ((p - q) . n) = ((p . n) - (q . n)) by NORMSP_1:def 3;

 definition

 let L be non empty ZeroStr;

 :: POLYNOM3:def7

 func 0_. (L) -> sequence of L equals ( NAT --> ( 0. L));

 coherence ;

 end

 registration

 let L be non empty ZeroStr;

 cluster ( 0_. L) -> finite-Support;

 coherence

 proof

 take 0 ;

 let i be Nat;

 assume i >= 0 ;

 i in NAT by ORDINAL1:def 12;

 hence thesis by FUNCOP_1: 7;

 end;

 end

 theorem :: POLYNOM3:28



 Th26: for L be right_zeroed non empty addLoopStr holds for p be sequence of L holds (p + ( 0_. L)) = p

 proof

 let L be right_zeroed non empty addLoopStr;

 let p be sequence of L;

 now

 let n be Element of NAT ;



 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;

 end;

 hence thesis;

 end;

 theorem :: POLYNOM3:29



 Th27: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be sequence of L holds (p - p) = ( 0_. L)

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 let p be sequence of L;

 now

 let n be Element of NAT ;



 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;

 end;

 hence thesis;

 end;

 definition

 let L be non empty multLoopStr_0;

 :: POLYNOM3:def8

 func 1_. (L) -> sequence of L equals (( 0_. L) +* ( 0 ,( 1. L)));

 coherence ;

 end

 registration

 let L be non empty multLoopStr_0;

 cluster ( 1_. L) -> finite-Support;

 coherence

 proof

 take 1;

 let i be Nat;



 A1: i in NAT by ORDINAL1:def 12;

 assume i >= 1;



 hence (( 1_. L) . i) = (( 0_. L) . i) by FUNCT_7: 32

 .= ( 0. L) by A1, FUNCOP_1: 7;

 end;

 end

 theorem :: POLYNOM3:30



 Th28: for L be non empty multLoopStr_0 holds (( 1_. L) . 0 ) = ( 1. L) & for n be Nat st n <> 0 holds (( 1_. L) . n) = ( 0. L)

 proof

 let L be non empty multLoopStr_0;

 0 in NAT ;

 then 0 in ( dom ( 0_. L)) by FUNCT_2:def 1;

 hence (( 1_. L) . 0 ) = ( 1. L) by FUNCT_7: 31;

 let n be Nat;



 A1: n in NAT by ORDINAL1:def 12;

 assume n <> 0 ;



 hence (( 1_. L) . n) = (( 0_. L) . n) by FUNCT_7: 32

 .= ( 0. L) by A1, FUNCOP_1: 7;

 end;

 definition

 let L be non empty doubleLoopStr;

 let p,q be sequence of L;

 :: POLYNOM3:def9

 func p *' q -> sequence of L means

 : Def9: for i be Element of NAT holds ex r be FinSequence of the carrier of L st ( len r) = (i + 1) & (it . i) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k)));

 existence

 proof

 defpred P[ Element of NAT , Element of L] means ex r be FinSequence of the carrier of L st ( len r) = ($1 + 1) & $2 = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . (($1 + 1) -' k)));



 A1: for i be Element of NAT holds ex v be Element of L st P[i, v]

 proof

 let i be Element of NAT ;

 deffunc F( Nat) = ((p . ($1 -' 1)) * (q . ((i + 1) -' $1)));

 consider r be FinSequence of the carrier of L such that

 A2: ( len r) = (i + 1) and

 A3: for k be Nat st k in ( dom r) holds (r . k) = F(k) from FINSEQ_2:sch 1;

 take v = ( Sum r);

 take r;

 thus ( len r) = (i + 1) by A2;

 thus v = ( Sum r);

 let k be Element of NAT ;

 assume k in ( dom r);

 hence thesis by A3;

 end;

 consider f be sequence of the carrier of L such that

 A4: for i be Element of NAT holds P[i, (f . i)] from FUNCT_2:sch 3( A1);

 take f;

 thus thesis by A4;

 end;

 uniqueness

 proof

 let p1,p2 be sequence of L such that

 A5: for i be Element of NAT holds ex r be FinSequence of the carrier of L st ( len r) = (i + 1) & (p1 . i) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) and

 A6: for i be Element of NAT holds ex r be FinSequence of the carrier of L st ( len r) = (i + 1) & (p2 . i) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k)));

 now

 let i be Element of NAT ;

 consider r1 be FinSequence of the carrier of L such that

 A7: ( len r1) = (i + 1) and

 A8: (p1 . i) = ( Sum r1) and

 A9: for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by A5;

 consider r2 be FinSequence of the carrier of L such that

 A10: ( len r2) = (i + 1) and

 A11: (p2 . i) = ( Sum r2) and

 A12: for k be 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

 let k be Nat;

 assume

 A14: k in ( dom r1);



 hence (r1 . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by A9

 .= (r2 . k) by A12, A13, A14;

 end;

 hence (p1 . i) = (p2 . i) by A8, A11, A13, FINSEQ_1: 13;

 end;

 hence p1 = p2;

 end;

 end

 registration

 let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

 let p,q be Polynomial of L;

 cluster (p *' q) -> finite-Support;

 coherence

 proof

 take s = (( len p) + ( len q));

 let i be Nat;

 i in NAT by ORDINAL1:def 12;

 then

 consider r be FinSequence of the carrier of L such that

 A1: ( len r) = (i + 1) and

 A2: ((p *' q) . i) = ( Sum r) and

 A3: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by Def9;

 assume i >= s;

 then ( len p) <= (i - ( len q)) by XREAL_1: 19;

 then

 A4: ( - ( len p)) >= ( - (i - ( len q))) by XREAL_1: 24;

 now

 let k be Element of NAT ;

 assume

 A5: k in ( dom r);

 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;

 per cases ;

 suppose (k -' 1) < ( len p);

 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;

 end;

 suppose (k -' 1) >= ( len p);

 then (p . (k -' 1)) = ( 0. L) by ALGSEQ_1: 8;

 hence (r . k) = ( 0. L) by A6;

 end;

 end;

 hence thesis by A2, Th1;

 end;

 end

 theorem :: POLYNOM3:31



 Th29: for L be Abelian add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for p,q,r be sequence of L holds (p *' (q + r)) = ((p *' q) + (p *' r))

 proof

 let L be Abelian add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let p,q,r be sequence of L;

 now

 let i be Element of NAT ;

 consider r1 be 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 be 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 be FinSequence of the carrier of L such that

 A5: ( len r3) = (i + 1) and

 A6: ((p *' r) . i) = ( Sum r3) and

 A7: for k be Element of NAT st k in ( dom r3) holds (r3 . k) = ((p . (k -' 1)) * (r . ((i + 1) -' k))) by Def9;

 consider r2 be FinSequence of the carrier of L such that

 A8: ( len r2) = (i + 1) and

 A9: ((p *' q) . i) = ( Sum r2) and

 A10: for k be 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

 let k be Nat;

 assume

 A12: k in ( dom r1);

 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;

 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;

 end;

 hence thesis;

 end;

 theorem :: POLYNOM3:32



 Th30: for L be Abelian add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds for p,q,r be sequence of L holds ((p + q) *' r) = ((p *' r) + (q *' r))

 proof

 let L be Abelian add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr;

 let p,q,r be sequence of L;

 now

 let i be Element of NAT ;

 consider r1 be 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 be 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 be FinSequence of the carrier of L such that

 A5: ( len r3) = (i + 1) and

 A6: ((q *' r) . i) = ( Sum r3) and

 A7: for k be Element of NAT st k in ( dom r3) holds (r3 . k) = ((q . (k -' 1)) * (r . ((i + 1) -' k))) by Def9;

 consider r2 be FinSequence of the carrier of L such that

 A8: ( len r2) = (i + 1) and

 A9: ((p *' r) . i) = ( Sum r2) and

 A10: for k be 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

 let k be Nat;

 assume

 A12: k in ( dom r1);

 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;

 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;

 end;

 hence thesis;

 end;

 theorem :: POLYNOM3:33



 Th31: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive non empty doubleLoopStr holds for p,q,r be sequence of L holds ((p *' q) *' r) = (p *' (q *' r))

 proof

 let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive non empty doubleLoopStr;

 let p,q,r be sequence of L;

 now

 let i be Element of NAT ;

 deffunc F( Nat) = (( Decomp (($1 -' 1),2)) ^^ ($1 |-> <*((i + 1) -' $1)*>) qua FinSequence of (1 -tuples_on NAT ));

 consider f2 be FinSequence of (((2 + 1) -tuples_on NAT ) * ) such that

 A1: ( len f2) = (i + 1) and

 A2: for k be Nat st k in ( dom f2) holds (f2 . k) = F(k) from FINSEQ_2:sch 1;



 A3: ( dom f2) = ( Seg (i + 1)) by A1, FINSEQ_1:def 3;

 reconsider f2 as FinSequence of ((3 -tuples_on NAT ) * );

 deffunc F( Nat) = ((((i + 2) -' $1) |-> <*($1 -' 1)*>) ^^ ( Decomp (((i + 1) -' $1),2)));

 consider g2 be FinSequence of (((1 + 2) -tuples_on NAT ) * ) such that

 A4: ( len g2) = (i + 1) and

 A5: for k be Nat st k in ( dom g2) holds (g2 . k) = F(k) from FINSEQ_2:sch 1;



 A6: ( dom g2) = ( Seg (i + 1)) by A4, FINSEQ_1:def 3;

 reconsider g2 as FinSequence of ((3 -tuples_on NAT ) * );

 consider r2 be 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 be 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

 let j be Nat;



 A13: ( dom (j |-> <*((i + 1) -' j)*>)) = ( Seg j) by FUNCOP_1: 13;

 assume

 A14: j in ( dom ( Card f2));

 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 qua Nat + (j - 1));

 then

 A23: ((i + 1) - (((i + 1) - j) + 1)) >= 0 by A16, XREAL_1: 48;



 then

 A24: (((i + 1) -' lj) + 1) = (( 0 qua Nat + (j - 1)) + 1) by A4, A19, XREAL_0:def 2

 .= j;

 (((i + 1) - j) + 1) >= ( 0 qua Nat + 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;

 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

 let y be object;

 thus y in ( rng ( FlattenSeq f2)) implies y in ( rng ( FlattenSeq g2))

 proof

 assume y in ( rng ( FlattenSeq f2));

 then

 consider x be Nat such that

 A35: x in ( dom ( FlattenSeq f2)) and

 A36: (( FlattenSeq f2) . x) = y by FINSEQ_2: 10;

 consider i1,j1 be 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) -' i2) |-> <*(i2 -' 1)*>)) = ( Seg ((i + 2) -' i2)) 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) -' i2) + 1) = (((i + 1) - i2) + 1) by XREAL_0:def 2

 .= ((i + (1 + 1)) - i2);

 ((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: i2 in ( Seg (i + 1)) by A50, FINSEQ_1: 1;

 then

 A55: (g2 . i2) = ((((i + 2) -' i2) |-> <*(i2 -' 1)*>) ^^ ( Decomp (((i + 1) -' i2),2))) by A5, A6;

 (i1 -' j1) <= ((i + 1) -' i2) by A48, NAT_D: 42;

 then 1 <= ((i1 -' j1) + 1) & ((i1 -' j1) + 1) <= (((i + 1) -' i2) + 1) by NAT_1: 11, XREAL_1: 6;

 then

 A56: j2 in ( Seg (((i + 1) -' i2) + 1)) by FINSEQ_1: 1;

 then

 A57: j2 in ( Seg ((i + 2) -' i2)) by A52, XREAL_0:def 2;

 ( dom ( Decomp (((i + 1) -' i2),2))) = ( Seg ( len ( Decomp (((i + 1) -' i2),2)))) by FINSEQ_1:def 3

 .= ( Seg (((i + 1) -' i2) + 1)) by Th9

 .= ( Seg ((i + 2) -' i2)) by A52, XREAL_0:def 2;

 then ( dom (g2 . i2)) = (( Seg ((i + 2) -' i2)) /\ ( Seg ((i + 2) -' i2))) by A55, A44, PRE_POLY:def 4;

 then

 A58: j2 in ( dom (g2 . i2)) by A56, A52, XREAL_0:def 2;



 then

 A59: ((g2 . i2) . j2) = (((((i + 2) -' i2) |-> <*(i2 -' 1)*>) . j2) ^ (( Decomp (((i + 1) -' i2),2)) . j2)) by A55, PRE_POLY:def 4

 .= ( <*(i2 -' 1)*> ^ (( Decomp (((i + 1) -' i2),2)) . j2)) by A57, FUNCOP_1: 7

 .= ( <*(i2 -' 1)*> ^ <*(j2 -' 1), ((((i + 1) -' i2) + 1) -' j2)*>) 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;

 i2 in ( dom g2) by A4, A54, FINSEQ_1:def 3;

 then

 A60: (( Sum ( Card (g2 | (i2 -' 1)))) + j2) in ( dom ( FlattenSeq g2)) & ((g2 . i2) . j2) = (( FlattenSeq g2) . (( Sum ( Card (g2 | (i2 -' 1)))) + j2)) 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 thesis by A59, A60, FUNCT_1:def 3;

 end;

 assume y in ( rng ( FlattenSeq g2));

 then

 consider x be Nat such that

 A61: x in ( dom ( FlattenSeq g2)) and

 A62: (( FlattenSeq g2) . x) = y by FINSEQ_2: 10;

 consider i1,j1 be 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 (i2 |-> <*((i + 1) -' i2)*>)) = ( Seg i2) by FUNCOP_1: 13;



 A80: 1 <= i1 by A69, FINSEQ_1: 1;

 then

 A81: j2 in ( Seg i2) by A78, FINSEQ_1: 1;

 then

 A82: j2 in ( Seg ((i2 -' 1) + 1)) by A80, A78, XREAL_1: 235, XXREAL_0: 2;

 ((j1 -' 1) + i1) >= 1 by A80, A78, XXREAL_0: 2;

 then

 A83: i2 in ( Seg (i + 1)) by A75, FINSEQ_1: 1;

 then

 A84: (f2 . i2) = (( Decomp ((i2 -' 1),2)) ^^ (i2 |-> <*((i + 1) -' i2)*>)) by A2, A3;

 ( dom ( Decomp ((i2 -' 1),2))) = ( Seg ( len ( Decomp ((i2 -' 1),2)))) by FINSEQ_1:def 3

 .= ( Seg ((i2 -' 1) + 1)) by Th9

 .= ( Seg i2) by A80, A78, XREAL_1: 235, XXREAL_0: 2;

 then ( dom (f2 . i2)) = (( Seg i2) /\ ( Seg i2)) by A84, A79, PRE_POLY:def 4;

 then

 A85: j2 in ( dom (f2 . i2)) by A80, A78, FINSEQ_1: 1;

 i2 in ( dom f2) by A1, A83, FINSEQ_1:def 3;

 then

 A86: (( Sum ( Card (f2 | (i2 -' 1)))) + j2) in ( dom ( FlattenSeq f2)) & ((f2 . i2) . j2) = (( FlattenSeq f2) . (( Sum ( Card (f2 | (i2 -' 1)))) + j2)) by A85, PRE_POLY: 30;

 ((f2 . i2) . j2) = ((( Decomp ((i2 -' 1),2)) . j2) ^ ((i2 |-> <*((i + 1) -' i2)*>) . j2)) by A84, A85, PRE_POLY:def 4

 .= ((( Decomp ((i2 -' 1),2)) . j2) ^ <*((i + 1) -' i2)*>) by A81, FUNCOP_1: 7

 .= ( <*(j2 -' 1), (((i2 -' 1) + 1) -' j2)*> ^ <*((i + 1) -' i2)*>) by A82, Th14

 .= <*(j2 -' 1), (((i2 -' 1) + 1) -' j2), ((i + 1) -' i2)*> 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;

 end;

 then

 A87: ( rng ( FlattenSeq f2)) = ( rng ( FlattenSeq g2)) by TARSKI: 2;

 now



 A88: ((i + 1) + 1) >= (i + 1) by NAT_1: 11;

 let x,y be object;

 assume that

 A89: x in ( dom ( FlattenSeq g2)) and

 A90: y in ( dom ( FlattenSeq g2)) and

 A91: (( FlattenSeq g2) . x) = (( FlattenSeq g2) . y);

 consider i1,j1 be 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 be 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;

 end;

 then

 A115: ( FlattenSeq g2) is one-to-one by FUNCT_1:def 4;



 A116: w is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

 ( len ( FlattenSeq f2)) = ( Sum ( Card f2)) by PRE_POLY: 27

 .= ( Sum w) by A33, Th3, A116

 .= ( 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 be Permutation of ( dom ( FlattenSeq g2)) such that

 A117: ( FlattenSeq f2) = (( FlattenSeq g2) * P) by RFINSEQ: 4;



 A118: ( dom ( Card g2)) = ( dom g2) by CARD_3:def 2;

 then

 A119: ( len ( Card g2)) = ( len g2) by FINSEQ_3: 29;

 consider r1 be FinSequence of the carrier of L such that

 A120: ( len r1) = (i + 1) and

 A121: (((p *' q) *' r) . i) = ( Sum r1) and

 A122: for k be Element of NAT st k in ( dom r1) holds (r1 . k) = (((p *' q) . (k -' 1)) * (r . ((i + 1) -' k))) by Def9;



 A123: ( dom r1) = ( Seg (i + 1)) by A120, FINSEQ_1:def 3;

 deffunc F( Nat) = ( prodTuples (p,q,r,(f2 /. $1) qua Element of ((3 -tuples_on NAT ) * )));

 consider f1 be FinSequence of (the carrier of L * ) such that

 A124: ( len f1) = ( len f2) and

 A125: for k be Nat st k in ( dom f1) holds (f1 . k) = F(k) from FINSEQ_2:sch 1;



 A126: ( dom f1) = ( Seg ( len f2)) by A124, FINSEQ_1:def 3;

 A127:

 now

 let j be Nat;



 A128: ( dom (j |-> <*((i + 1) -' j)*>)) = ( Seg j) by FUNCOP_1: 13;

 consider r3 be FinSequence of the carrier of L such that

 A129: ( len r3) = ((j -' 1) + 1) and

 A130: ((p *' q) . (j -' 1)) = ( Sum r3) and

 A131: for k be Element of NAT st k in ( dom r3) holds (r3 . k) = ((p . (k -' 1)) * (q . (((j -' 1) + 1) -' k))) by Def9;

 assume

 A132: j in ( dom r1);

 then

 A133: 1 <= j by A123, FINSEQ_1: 1;

 then

 A134: ( len r3) = j by A129, XREAL_1: 235;

 ( len ( Decomp ((j -' 1),2))) = ((j -' 1) + 1) by Th9

 .= j by A133, XREAL_1: 235;

 then

 A135: ( dom ( Decomp ((j -' 1),2))) = ( Seg j) by FINSEQ_1:def 3;



 A136: ( dom r1) = ( dom f1) by A120, A1, A124, FINSEQ_3: 29;



 then

 A137: (f1 /. j) = (f1 . j) by A132, PARTFUN1:def 6

 .= ( prodTuples (p,q,r,(f2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) by A1, A125, A126, A123, A132;

 ( dom f1) = ( dom f2) by A124, FINSEQ_3: 29;



 then

 A138: (f2 /. j) = (f2 . j) by A132, A136, PARTFUN1:def 6

 .= (( Decomp ((j -' 1),2)) ^^ (j |-> <*((i + 1) -' j)*>)) by A2, A3, A123, A132;



 then

 A139: ( dom (f2 /. j)) = (( dom ( Decomp ((j -' 1),2))) /\ ( dom (j |-> <*((i + 1) -' j)*>))) by PRE_POLY:def 4

 .= ( Seg j) by A135, A128;



 A140: ( len ( prodTuples (p,q,r,(f2 /. j) qua Element of ((3 -tuples_on NAT ) * )))) = ( len (f2 /. j) qua Element of ((3 -tuples_on NAT ) * )) by Def5

 .= j by A132, A139, FINSEQ_1:def 3;

 then

 A141: ( dom ( prodTuples (p,q,r,(f2 /. j) qua Element of ((3 -tuples_on NAT ) * )))) = ( Seg j) by FINSEQ_1:def 3;



 A142: ( dom (r3 * (r . ((i + 1) -' j)))) = ( dom r3) by POLYNOM1:def 2;

 A143:

 now

 let k be Nat;

 assume

 A144: k in ( dom ( prodTuples (p,q,r,(f2 /. j) qua Element of ((3 -tuples_on NAT ) * ))));



 then

 A145: ((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) = ((f2 /. j) . k) by A139, A141, PARTFUN1:def 6

 .= ((( Decomp ((j -' 1),2)) . k) ^ ((j |-> <*((i + 1) -' j)*>) . k)) by A138, A139, A141, A144, PRE_POLY:def 4

 .= ( <*(k -' 1), (((j -' 1) + 1) -' k)*> ^ ((j |-> <*((i + 1) -' j)*>) . k)) by A129, A134, A141, A144, Th14

 .= ( <*(k -' 1), (((j -' 1) + 1) -' k)*> ^ <*((i + 1) -' j)*>) by A141, A144, 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) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ))) by A145, FINSEQ_1: 45;

 then 1 in ( dom ((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k)) by FINSEQ_1:def 3;



 then

 A146: (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 1) = (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) . 1) by PARTFUN1:def 6

 .= (k -' 1) by A145, FINSEQ_1: 45;



 A147: k in ( dom r3) by A134, A141, A144, FINSEQ_1:def 3;



 then

 A148: (r3 /. k) = (r3 . k) by PARTFUN1:def 6

 .= ((p . (k -' 1)) * (q . (((j -' 1) + 1) -' k))) by A131, A147;

 3 in ( Seg 3) by ENUMSET1:def 1, FINSEQ_3: 1;

 then 3 in ( Seg ( len ((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ))) by A145, FINSEQ_1: 45;

 then 3 in ( dom ((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k)) by FINSEQ_1:def 3;



 then

 A149: (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 3) = (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) . 3) by PARTFUN1:def 6

 .= ((i + 1) -' j) by A145, FINSEQ_1: 45;

 2 in ( Seg 3) by ENUMSET1:def 1, FINSEQ_3: 1;

 then 2 in ( Seg ( len ((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ))) by A145, FINSEQ_1: 45;

 then 2 in ( dom ((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k)) by FINSEQ_1:def 3;



 then

 A150: (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 2) = (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) . 2) by PARTFUN1:def 6

 .= (((j -' 1) + 1) -' k) by A145, FINSEQ_1: 45;



 thus (( prodTuples (p,q,r,(f2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) . k) = (((p . (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 1)) * (q . (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 2))) * (r . (((f2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 3))) by A139, A141, A144, Def5

 .= ((r3 * (r . ((i + 1) -' j))) /. k) by A147, A148, A146, A150, A149, POLYNOM1:def 2

 .= ((r3 * (r . ((i + 1) -' j))) . k) by A142, A147, PARTFUN1:def 6;

 end;

 ( len f1) = ( len ( Sum f1)) by MATRLIN:def 6;

 then

 A151: ( dom f1) = ( dom ( Sum f1)) by FINSEQ_3: 29;

 ( len (r3 * (r . ((i + 1) -' j)))) = ( len r3) by A142, FINSEQ_3: 29;

 then

 A152: ( prodTuples (p,q,r,(f2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) = (r3 * (r . ((i + 1) -' j))) by A140, A134, A143, FINSEQ_2: 9;

 (((p *' q) . (j -' 1)) * (r . ((i + 1) -' j))) = ( Sum (r3 * (r . ((i + 1) -' j)))) by A130, POLYNOM1: 13;



 hence (r1 . j) = ( Sum (r3 * (r . ((i + 1) -' j)))) by A122, A132

 .= (( Sum f1) /. j) by A132, A151, A136, A137, A152, MATRLIN:def 6

 .= (( Sum f1) . j) by A132, A151, A136, PARTFUN1:def 6;

 end;

 deffunc F( Nat) = ( prodTuples (p,q,r,(g2 /. $1) qua Element of ((3 -tuples_on NAT ) * )));

 consider g1 be FinSequence of (the carrier of L * ) such that

 A153: ( len g1) = ( len g2) and

 A154: for k be Nat st k in ( dom g1) holds (g1 . k) = F(k) from FINSEQ_2:sch 1;



 A155: ( dom g1) = ( Seg ( len g2)) by A153, FINSEQ_1:def 3;

 A156:

 now

 let j be Nat;



 A157: ( dom (((i + 2) -' j) |-> <*(j -' 1)*>)) = ( Seg ((i + 2) -' j)) by FUNCOP_1: 13;

 consider r3 be FinSequence of the carrier of L such that

 A158: ( len r3) = (((i + 1) -' j) + 1) and

 A159: ((q *' r) . ((i + 1) -' j)) = ( Sum r3) and

 A160: for k be Element of NAT st k in ( dom r3) holds (r3 . k) = ((q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k))) by Def9;

 assume

 A161: j in ( dom r2);

 then

 A162: j <= (i + 1) by A10, FINSEQ_1: 1;

 ((i + 1) + 1) >= (i + 1) by NAT_1: 11;

 then ((i + 1) + 1) >= j by A162, XXREAL_0: 2;

 then

 A163: ((i + 2) - j) >= 0 by XREAL_1: 48;

 ((i + 1) - j) >= 0 by A162, XREAL_1: 48;



 then

 A164: (((i + 1) -' j) + 1) = (((i + 1) - j) + 1) by XREAL_0:def 2

 .= ((i + 2) -' j) by A163, XREAL_0:def 2;

 then ( len ( Decomp (((i + 1) -' j),2))) = ((i + 2) -' j) by Th9;

 then

 A165: ( dom ( Decomp (((i + 1) -' j),2))) = ( Seg ((i + 2) -' j)) by FINSEQ_1:def 3;



 A166: ( dom r2) = ( dom g1) by A7, A4, A153, FINSEQ_3: 29;



 then

 A167: (g1 /. j) = (g1 . j) by A161, PARTFUN1:def 6

 .= ( prodTuples (p,q,r,(g2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) by A4, A154, A155, A10, A161;

 ( dom g1) = ( dom g2) by A153, FINSEQ_3: 29;



 then

 A168: (g2 /. j) = (g2 . j) by A161, A166, PARTFUN1:def 6

 .= ((((i + 2) -' j) |-> <*(j -' 1)*>) ^^ ( Decomp (((i + 1) -' j),2))) by A5, A6, A10, A161;



 then

 A169: ( 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 A165, A157;



 A170: ( len ( prodTuples (p,q,r,(g2 /. j) qua Element of ((3 -tuples_on NAT ) * )))) = ( len (g2 /. j) qua Element of ((3 -tuples_on NAT ) * )) by Def5

 .= ((i + 2) -' j) by A169, FINSEQ_1:def 3;

 then

 A171: ( dom ( prodTuples (p,q,r,(g2 /. j) qua Element of ((3 -tuples_on NAT ) * )))) = ( Seg ((i + 2) -' j)) by FINSEQ_1:def 3;



 A172: ( dom ((p . (j -' 1)) * r3)) = ( dom r3) by POLYNOM1:def 1;

 A173:

 now

 let k be Nat;

 assume

 A174: k in ( dom ( prodTuples (p,q,r,(g2 /. j) qua Element of ((3 -tuples_on NAT ) * ))));



 then

 A175: ((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) = ((g2 /. j) . k) by A169, A171, PARTFUN1:def 6

 .= (((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ (( Decomp (((i + 1) -' j),2)) . k)) by A168, A169, A171, A174, PRE_POLY:def 4

 .= (((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ <*(k -' 1), ((((i + 1) -' j) + 1) -' k)*>) by A164, A171, A174, Th14

 .= ( <*(j -' 1)*> ^ <*(k -' 1), ((((i + 1) -' j) + 1) -' k)*>) by A171, A174, 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) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ))) by A175, FINSEQ_1: 45;

 then 1 in ( dom ((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k)) by FINSEQ_1:def 3;



 then

 A176: (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 1) = (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) . 1) by PARTFUN1:def 6

 .= (j -' 1) by A175, FINSEQ_1: 45;



 A177: k in ( dom r3) by A158, A164, A171, A174, FINSEQ_1:def 3;



 then

 A178: (r3 /. k) = (r3 . k) by PARTFUN1:def 6

 .= ((q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k))) by A160, A177;

 3 in ( Seg 3) by ENUMSET1:def 1, FINSEQ_3: 1;

 then 3 in ( Seg ( len ((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ))) by A175, FINSEQ_1: 45;

 then 3 in ( dom ((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k)) by FINSEQ_1:def 3;



 then

 A179: (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 3) = (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) . 3) by PARTFUN1:def 6

 .= ((((i + 1) -' j) + 1) -' k) by A175, FINSEQ_1: 45;

 2 in ( Seg 3) by ENUMSET1:def 1, FINSEQ_3: 1;

 then 2 in ( Seg ( len ((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ))) by A175, FINSEQ_1: 45;

 then 2 in ( dom ((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k)) by FINSEQ_1:def 3;



 then

 A180: (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 2) = (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) . 2) by PARTFUN1:def 6

 .= (k -' 1) by A175, FINSEQ_1: 45;



 thus (( prodTuples (p,q,r,(g2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) . k) = (((p . (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 1)) * (q . (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 2))) * (r . (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 3))) by A169, A171, A174, Def5

 .= ((p . (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 1)) * ((q . (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 2)) * (r . (((g2 /. j) qua Element of ((3 -tuples_on NAT ) * ) /. k) qua Element of (3 -tuples_on NAT ) /. 3)))) by GROUP_1:def 3

 .= (((p . (j -' 1)) * r3) /. k) by A177, A178, A176, A180, A179, POLYNOM1:def 1

 .= (((p . (j -' 1)) * r3) . k) by A172, A177, PARTFUN1:def 6;

 end;

 ( len g1) = ( len ( Sum g1)) by MATRLIN:def 6;

 then

 A181: ( dom g1) = ( dom ( Sum g1)) by FINSEQ_3: 29;

 ( len ((p . (j -' 1)) * r3)) = ( len r3) by A172, FINSEQ_3: 29;

 then

 A182: ( prodTuples (p,q,r,(g2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) = ((p . (j -' 1)) * r3) by A158, A164, A170, A173, FINSEQ_2: 9;

 ((p . (j -' 1)) * ((q *' r) . ((i + 1) -' j))) = ( Sum ((p . (j -' 1)) * r3)) by A159, POLYNOM1: 12;



 hence (r2 . j) = ( Sum ((p . (j -' 1)) * r3)) by A9, A161

 .= (( Sum g1) /. j) by A161, A181, A166, A167, A182, MATRLIN:def 6

 .= (( Sum g1) . j) by A161, A181, A166, PARTFUN1:def 6;

 end;



 A183: ( dom ( Card g2)) = ( Seg (i + 1)) by A4, A118, FINSEQ_1:def 3;

 A184:

 now

 let j be Nat;

 assume

 A185: j in ( dom ( Card g2));

 then

 A186: j in ( dom g1) by A4, A153, A183, FINSEQ_1:def 3;

 (g1 . j) = ( prodTuples (p,q,r,(g2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) by A4, A154, A155, A183, A185;



 then

 A187: ( len (g1 . j)) = ( len (g2 /. j)) by Def5

 .= ( len (g2 . j)) by A118, A185, PARTFUN1:def 6;



 thus (( Card g2) . j) = ( len (g2 . j)) by A118, A185, CARD_3:def 2

 .= (( Card g1) . j) by A186, A187, CARD_3:def 2;

 end;



 A188: ( dom ( Card g1)) = ( dom g1) by CARD_3:def 2;

 then ( len ( Card g1)) = ( len g1) by FINSEQ_3: 29;

 then

 A189: ( Card g2) = ( Card g1) by A153, A119, A184, FINSEQ_2: 9;

 then

 A190: ( len ( FlattenSeq g2)) = ( len ( FlattenSeq g1)) by PRE_POLY: 28;

 then

 A191: ( dom ( FlattenSeq g2)) = ( dom ( FlattenSeq g1)) by FINSEQ_3: 29;

 then

 reconsider P as Permutation of ( dom ( FlattenSeq g1));



 A192: ( dom ( FlattenSeq g1)) = ( Seg ( len ( FlattenSeq g1))) by FINSEQ_1:def 3;

 A193:

 now

 let j be Nat;

 assume

 A194: j in ( dom ( FlattenSeq g1));

 then

 consider i1,j1 be Nat such that

 A195: i1 in ( dom g1) and

 A196: j1 in ( dom (g1 . i1)) and

 A197: j = (( Sum ( Card (g1 | (i1 -' 1)))) + j1) and

 A198: ((g1 . i1) . j1) = (( FlattenSeq g1) . j) by PRE_POLY: 29;



 A199: j in ( dom ( FlattenSeq g2)) by A190, A192, A194, FINSEQ_1:def 3;

 then

 consider i2,j2 be Nat such that

 A200: i2 in ( dom g2) & j2 in ( dom (g2 . i2)) and

 A201: j = (( Sum ( Card (g2 | (i2 -' 1)))) + j2) and

 A202: ((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 A197, A201, Th16;

 then

 A203: i1 = i2 & j1 = j2 by A189, A195, A196, A200, Th21;

 i1 in ( Seg ( len g2)) by A153, A195, FINSEQ_1:def 3;

 then

 A204: i1 in ( dom g2) by FINSEQ_1:def 3;



 A205: (g1 . i1) = ( prodTuples (p,q,r,(g2 /. i1) qua Element of ((3 -tuples_on NAT ) * ))) by A154, A195;



 then ( len (g1 . i1)) = ( len (g2 /. i1)) by Def5

 .= ( len (g2 . i1)) by A188, A118, A189, A195, PARTFUN1:def 6;

 then j1 in ( Seg ( len (g2 . i1))) by A196, FINSEQ_1:def 3;

 then

 A206: j1 in ( Seg ( len (g2 /. i1))) by A204, PARTFUN1:def 6;

 then j1 in ( dom (g2 /. i1)) by FINSEQ_1:def 3;



 then

 A207: ((g2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) = ((g2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) . j1) by PARTFUN1:def 6

 .= ((g2 . i1) . j1) by A204, PARTFUN1:def 6

 .= (( FlattenSeq g2) /. j) by A199, A202, A203, PARTFUN1:def 6;

 ( Seg ( len (g2 /. i1))) = ( dom (g2 /. i1)) by FINSEQ_1:def 3;



 hence (( FlattenSeq g1) . j) = (((p . (((g2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) qua Element of (3 -tuples_on NAT ) /. 1)) * (q . (((g2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) qua Element of (3 -tuples_on NAT ) /. 2))) * (r . (((g2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) qua Element of (3 -tuples_on NAT ) /. 3))) by A198, A205, A206, Def5

 .= (( prodTuples (p,q,r,( FlattenSeq g2))) . j) by A191, A194, A207, Def5;

 end;



 A208: ( dom ( Card f2)) = ( dom f2) by CARD_3:def 2;

 then

 A209: ( len ( Card f2)) = ( len f2) by FINSEQ_3: 29;



 A210: ( dom ( Card f2)) = ( Seg (i + 1)) by A1, A208, FINSEQ_1:def 3;

 A211:

 now

 let j be Nat;

 assume

 A212: j in ( dom ( Card f2));

 then

 A213: j in ( dom f1) by A1, A124, A210, FINSEQ_1:def 3;

 (f1 . j) = ( prodTuples (p,q,r,(f2 /. j) qua Element of ((3 -tuples_on NAT ) * ))) by A1, A125, A126, A210, A212;



 then

 A214: ( len (f1 . j)) = ( len (f2 /. j)) by Def5

 .= ( len (f2 . j)) by A208, A212, PARTFUN1:def 6;



 thus (( Card f2) . j) = ( len (f2 . j)) by A208, A212, CARD_3:def 2

 .= (( Card f1) . j) by A213, A214, CARD_3:def 2;

 end;



 A215: ( dom ( Card f1)) = ( dom f1) by CARD_3:def 2;

 then ( len ( Card f1)) = ( len f1) by FINSEQ_3: 29;

 then

 A216: ( Card f2) = ( Card f1) by A124, A209, A211, FINSEQ_2: 9;

 then

 A217: ( len ( FlattenSeq f1)) = ( len ( FlattenSeq f2)) by PRE_POLY: 28;



 A218: ( Seg ( len ( FlattenSeq f1))) = ( dom ( FlattenSeq f1)) by FINSEQ_1:def 3;

 A219:

 now

 let j be Nat;

 assume

 A220: j in ( dom ( FlattenSeq f1));

 then

 consider i1,j1 be Nat such that

 A221: i1 in ( dom f1) and

 A222: j1 in ( dom (f1 . i1)) and

 A223: j = (( Sum ( Card (f1 | (i1 -' 1)))) + j1) and

 A224: ((f1 . i1) . j1) = (( FlattenSeq f1) . j) by PRE_POLY: 29;



 A225: j in ( dom ( FlattenSeq f2)) by A217, A34, A220, FINSEQ_1:def 3;

 then

 consider i2,j2 be Nat such that

 A226: i2 in ( dom f2) & j2 in ( dom (f2 . i2)) and

 A227: j = (( Sum ( Card (f2 | (i2 -' 1)))) + j2) and

 A228: ((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 A223, A227, Th16;

 then

 A229: i1 = i2 & j1 = j2 by A216, A221, A222, A226, Th21;

 i1 in ( Seg ( len f2)) by A124, A221, FINSEQ_1:def 3;

 then

 A230: i1 in ( dom f2) by FINSEQ_1:def 3;



 A231: (f1 . i1) = ( prodTuples (p,q,r,(f2 /. i1) qua Element of ((3 -tuples_on NAT ) * ))) by A125, A221;



 then ( len (f1 . i1)) = ( len (f2 /. i1)) by Def5

 .= ( len (f2 . i1)) by A215, A208, A216, A221, PARTFUN1:def 6;

 then j1 in ( Seg ( len (f2 . i1))) by A222, FINSEQ_1:def 3;

 then

 A232: j1 in ( Seg ( len (f2 /. i1))) by A230, PARTFUN1:def 6;

 then j1 in ( dom (f2 /. i1)) by FINSEQ_1:def 3;



 then

 A233: ((f2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) = ((f2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) . j1) by PARTFUN1:def 6

 .= ((f2 . i1) . j1) by A230, PARTFUN1:def 6

 .= (( FlattenSeq f2) /. j) by A225, A228, A229, PARTFUN1:def 6;

 ( Seg ( len (f2 /. i1))) = ( dom (f2 /. i1)) by FINSEQ_1:def 3;



 hence (( FlattenSeq f1) . j) = (((p . (((f2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) qua Element of (3 -tuples_on NAT ) /. 1)) * (q . (((f2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) qua Element of (3 -tuples_on NAT ) /. 2))) * (r . (((f2 /. i1) qua Element of ((3 -tuples_on NAT ) * ) /. j1) qua Element of (3 -tuples_on NAT ) /. 3))) by A224, A231, A232, Def5

 .= (((p . ((( FlattenSeq f2) /. j) /. 1)) * (q . ((( FlattenSeq f2) /. j) /. 2))) * (r . ((( FlattenSeq f2) /. j) /. 3))) by A233

 .= (( prodTuples (p,q,r,( FlattenSeq f2))) . j) by A217, A34, A218, A220, Def5;

 end;

 ( len ( Sum g1)) = (i + 1) by A4, A153, MATRLIN:def 6;

 then r2 = ( Sum g1) by A7, A156, FINSEQ_2: 9;

 then

 A234: ( Sum r2) = ( Sum ( FlattenSeq g1)) by POLYNOM1: 14;

 ( len ( FlattenSeq g1)) = ( len ( prodTuples (p,q,r,( FlattenSeq g2)))) by A190, Def5;

 then

 A235: ( FlattenSeq g1) = ( prodTuples (p,q,r,( FlattenSeq g2))) by A193, FINSEQ_2: 9;

 ( len ( FlattenSeq f1)) = ( len ( prodTuples (p,q,r,( FlattenSeq f2)))) by A217, Def5;

 then ( FlattenSeq f1) = ( prodTuples (p,q,r,( FlattenSeq f2))) by A219, FINSEQ_2: 9;

 then

 A236: ( FlattenSeq f1) = (( FlattenSeq g1) * P) by A235, A117, Th15;

 ( len ( Sum f1)) = (i + 1) by A1, A124, MATRLIN:def 6;

 then r1 = ( Sum f1) by A120, A127, FINSEQ_2: 9;

 then ( Sum r1) = ( Sum ( FlattenSeq f1)) by POLYNOM1: 14;

 hence (((p *' q) *' r) . i) = ((p *' (q *' r)) . i) by A121, A8, A234, A236, RLVECT_2: 7;

 end;

 hence thesis;

 end;

 definition

 let L be Abelian add-associative right_zeroed commutative non empty doubleLoopStr;

 let p,q be sequence of L;

 :: original: *'

 redefine

 func p *' q;

 commutativity

 proof

 let p,q be sequence of L;

 now

 let i be Element of NAT ;

 consider r1 be FinSequence of the carrier of L such that

 A1: ( len r1) = (i + 1) and

 A2: ((p *' q) . i) = ( Sum r1) and

 A3: for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by Def9;

 consider r2 be FinSequence of the carrier of L such that

 A4: ( len r2) = (i + 1) and

 A5: ((q *' p) . i) = ( Sum r2) and

 A6: for k be Element of NAT st k in ( dom r2) holds (r2 . k) = ((q . (k -' 1)) * (p . ((i + 1) -' k))) by Def9;

 now

 let k be Nat;

 assume

 A7: k in ( dom r1);

 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 qua Nat) 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 qua Nat + 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;

 end;

 then r1 = ( Rev r2) by A1, A4, FINSEQ_5:def 3;

 hence ((p *' q) . i) = ((q *' p) . i) by A2, A5, Th2;

 end;

 hence (p *' q) = (q *' p);

 end;

 end

 theorem :: POLYNOM3:34

 for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for p be sequence of L holds (p *' ( 0_. L)) = ( 0_. L)

 proof

 let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let p be sequence of L;

 now

 let i be Element of NAT ;

 consider r be FinSequence of the carrier of L such that ( len r) = (i + 1) and

 A1: ((p *' ( 0_. L)) . i) = ( Sum r) and

 A2: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (( 0_. L) . ((i + 1) -' k))) by Def9;

 now

 let k be Element of NAT ;

 assume k in ( dom r);



 hence (r . k) = ((p . (k -' 1)) * (( 0_. L) . ((i + 1) -' k))) by A2

 .= ((p . (k -' 1)) * ( 0. L)) by FUNCOP_1: 7

 .= ( 0. L);

 end;



 hence ((p *' ( 0_. L)) . i) = ( 0. L) by A1, Th1

 .= (( 0_. L) . i) by FUNCOP_1: 7;

 end;

 hence thesis;

 end;

 theorem :: POLYNOM3:35



 Th33: for L be add-associative right_zeroed well-unital right_complementable right-distributive non empty doubleLoopStr holds for p be sequence of L holds (p *' ( 1_. L)) = p

 proof

 let L be add-associative right_zeroed well-unital right_complementable right-distributive non empty doubleLoopStr;

 let p be sequence of L;

 now

 let i be Element of NAT ;

 consider r be 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 be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (( 1_. L) . ((i + 1) -' k))) by Def9;



 a1: r <> {} by A1;

 (i + 1) in ( Seg ( len r)) by A1, FINSEQ_1: 4;

 then

 A4: (i + 1) in ( dom r) by FINSEQ_1:def 3;

 now

 let k be Element of NAT ;

 assume k in ( dom ( Del (r,(i + 1))));

 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, Th28

 .= ( 0. L);

 end;

 then

 A11: ( Sum ( Del (r,(i + 1)))) = ( 0. L) by Th1;

 r = (( Del (r,(i + 1))) ^ <*(r . (i + 1))*>) by A1, 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 Th28

 .= (p . i);

 hence ((p *' ( 1_. L)) . i) = (p . i) by A2, A12, A11, RLVECT_1: 4;

 end;

 hence thesis;

 end;

 begin

 definition

 let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

 :: POLYNOM3:def10

 func Polynom-Ring L -> strict non empty doubleLoopStr means

 : Def10: (for x be set holds x in the carrier of it iff x is Polynomial of L) & (for x,y be Element of it , p,q be sequence of L st x = p & y = q holds (x + y) = (p + q)) & (for x,y be Element of it , p,q be sequence of L st x = p & y = q holds (x * y) = (p *' q)) & ( 0. it ) = ( 0_. L) & ( 1. it ) = ( 1_. L);

 existence

 proof



 A1: ( 0_. L) in the set of all x where x be Polynomial of L;

 then

 reconsider Ca = the set of all x where x be Polynomial of L as non empty set;

 reconsider Ze = ( 0_. L) as Element of Ca by A1;

 defpred P[ set, set, set] means ex p,q be Polynomial of L st p = $1 & q = $2 & $3 = (p + q);



 A2: for x,y be Element of Ca holds ex u be Element of Ca st P[x, y, u]

 proof

 let x,y be Element of Ca;

 x in Ca;

 then

 consider p be Polynomial of L such that

 A3: x = p;

 y in Ca;

 then

 consider q be Polynomial of L such that

 A4: y = q;

 (p + q) in Ca;

 then

 reconsider u = (p + q) as Element of Ca;

 take u, p, q;

 thus thesis by A3, A4;

 end;

 consider Ad be Function of [:Ca, Ca:], Ca such that

 A5: for x,y be Element of Ca holds P[x, y, (Ad . (x,y))] from BINOP_1:sch 3( A2);

 ( 1_. L) in the set of all x where x be Polynomial of L;

 then

 reconsider Un = ( 1_. L) as Element of Ca;

 defpred P[ set, set, set] means ex p,q be Polynomial of L st p = $1 & q = $2 & $3 = (p *' q);



 A6: for x,y be Element of Ca holds ex u be Element of Ca st P[x, y, u]

 proof

 let x,y be Element of Ca;

 x in Ca;

 then

 consider p be Polynomial of L such that

 A7: x = p;

 y in Ca;

 then

 consider q be Polynomial of L such that

 A8: y = q;

 (p *' q) in Ca;

 then

 reconsider u = (p *' q) as Element of Ca;

 take u, p, q;

 thus thesis by A7, A8;

 end;

 consider Mu be Function of [:Ca, Ca:], Ca such that

 A9: for x,y be Element of Ca holds P[x, y, (Mu . (x,y))] from BINOP_1:sch 3( A6);

 reconsider P = doubleLoopStr (# Ca, Ad, Mu, Un, Ze #) as strict non empty doubleLoopStr;

 take P;

 thus for x be set holds x in the carrier of P iff x is Polynomial of L

 proof

 let x be set;

 thus x in the carrier of P implies x is Polynomial of L

 proof

 assume x in the carrier of P;

 then ex p be Polynomial of L st x = p;

 hence thesis;

 end;

 thus thesis;

 end;

 thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds (x + y) = (p + q)

 proof

 let x,y be Element of P;

 let p,q be sequence of L;

 assume

 A10: x = p & y = q;

 ex p1,q1 be Polynomial of L st p1 = x & q1 = y & (Ad . (x,y)) = (p1 + q1) by A5;

 hence thesis by A10;

 end;

 thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds (x * y) = (p *' q)

 proof

 let x,y be Element of P;

 let p,q be sequence of L;

 assume

 A11: x = p & y = q;

 ex p1,q1 be Polynomial of L st p1 = x & q1 = y & (Mu . (x,y)) = (p1 *' q1) by A9;

 hence thesis by A11;

 end;

 thus ( 0. P) = ( 0_. L);

 thus thesis;

 end;

 uniqueness

 proof

 let P1,P2 be strict non empty doubleLoopStr such that

 A12: for x be set holds x in the carrier of P1 iff x is Polynomial of L and

 A13: for x,y be Element of P1, p,q be sequence of L st x = p & y = q holds (x + y) = (p + q) and

 A14: for x,y be Element of P1, p,q be 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 be set holds x in the carrier of P2 iff x is Polynomial of L and

 A17: for x,y be Element of P2, p,q be sequence of L st x = p & y = q holds (x + y) = (p + q) and

 A18: for x,y be Element of P2, p,q be sequence of L st x = p & y = q holds (x * y) = (p *' q) and

 A19: ( 0. P2) = ( 0_. L) & ( 1. P2) = ( 1_. L);

 A20:

 now

 let x be object;

 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;

 end;

 then

 A21: the carrier of P1 = the carrier of P2 by TARSKI: 2;

 A22:

 now

 let x be Element of P1, y be Element of P2;

 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));

 end;

 now

 let x be Element of P1, y be Element of P2;

 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));

 end;

 then the addF of P1 = the addF of P2 by A21, BINOP_1: 2;

 hence thesis by A15, A19, A21, A22, BINOP_1: 2;

 end;

 end

 registration

 let L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

 cluster ( Polynom-Ring L) -> Abelian;

 coherence

 proof

 let p,q be Element of ( Polynom-Ring L);

 reconsider p1 = p, q1 = q as sequence of L by Def10;



 thus (p + q) = (p1 + q1) by Def10

 .= (q + p) by Def10;

 end;

 end

 registration

 let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

 cluster ( Polynom-Ring L) -> add-associative;

 coherence

 proof

 let p,q,r be Element of ( Polynom-Ring L);

 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 Th24

 .= (p + (q + r)) by A1, Def10;

 end;

 cluster ( Polynom-Ring L) -> right_zeroed;

 coherence

 proof

 let p be Element of ( Polynom-Ring L);

 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 Th26;

 end;

 cluster ( Polynom-Ring L) -> right_complementable;

 coherence

 proof

 let p be Element of ( Polynom-Ring L);

 reconsider p1 = p as Polynomial of L by Def10;

 reconsider q = ( - p1) as Element of ( Polynom-Ring L) by Def10;

 take q;



 thus (p + q) = (p1 - p1) by Def10

 .= ( 0_. L) by Th27

 .= ( 0. ( Polynom-Ring L)) by Def10;

 end;

 end

 registration

 let L be Abelian add-associative right_zeroed right_complementable commutative distributive non empty doubleLoopStr;

 cluster ( Polynom-Ring L) -> commutative;

 coherence

 proof

 let p,q be Element of ( Polynom-Ring L);

 reconsider p1 = p, q1 = q as sequence of L by Def10;



 thus (p * q) = (p1 *' q1) by Def10

 .= (q * p) by Def10;

 end;

 end

 registration

 let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive non empty doubleLoopStr;

 cluster ( Polynom-Ring L) -> associative;

 coherence

 proof

 let p,q,r be Element of ( Polynom-Ring L);

 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 Th31

 .= (p * (q * r)) by A1, Def10;

 end;

 end

 theorem :: POLYNOM3:36



 Th33a: for L be add-associative right_zeroed well-unital right_complementable left-distributive non empty doubleLoopStr holds for p be sequence of L holds (( 1_. L) *' p) = p

 proof

 let L be add-associative right_zeroed well-unital right_complementable left-distributive non empty doubleLoopStr;

 let p be sequence of L;

 now

 let i be Element of NAT ;

 consider r be FinSequence of the carrier of L such that

 A1: ( len r) = (i + 1) and

 A2: ((( 1_. L) *' p) . i) = ( Sum r) and

 A3: for k be Element of NAT st k in ( dom r) holds (r . k) = ((( 1_. L) . (k -' 1)) * (p . ((i + 1) -' k))) by Def9;



 A4: 1 in ( dom r) by A1, CARD_1: 27, FINSEQ_5: 6;

 now

 let k be Element of NAT ;



 A5: (k + 1) >= 1 by NAT_1: 11;

 assume

 A6: k in ( dom ( Del (r,1)));

 then

 A7: k <> 0 by FINSEQ_3: 25;

 ( len ( Del (r,1))) = i by A1, A4, FINSEQ_3: 109;

 then

 A8: k <= i by A6, FINSEQ_3: 25;

 then (k + 1) <= (i + 1) by XREAL_1: 6;

 then

 A9: (k + 1) in ( dom r) by A1, A5, FINSEQ_3: 25;

 ( 0 + 1) <= k by A6, FINSEQ_3: 25;



 hence (( Del (r,1)) . k) = (r . (k + 1)) by A1, A4, A8, FINSEQ_3: 111

 .= ((( 1_. L) . ((k + 1) -' 1)) * (p . ((i + 1) -' (k + 1)))) by A3, A9

 .= ((( 1_. L) . k) * (p . ((i + 1) -' (k + 1)))) by NAT_D: 34

 .= (( 0. L) * (p . ((i + 1) -' (k + 1)))) by A7, Th28

 .= ( 0. L);

 end;

 then

 A10: ( Sum ( Del (r,1))) = ( 0. L) by Th1;

 r = ( <*(r . 1)*> ^ ( Del (r,1))) by A1, FINSEQ_5: 86, CARD_1: 27

 .= ( <*(r /. 1)*> ^ ( Del (r,1))) by A4, PARTFUN1:def 6;



 then

 A11: ( Sum r) = (( Sum <*(r /. 1)*>) + ( Sum ( Del (r,1)))) by RLVECT_1: 41

 .= ((r /. 1) + ( Sum ( Del (r,1)))) by RLVECT_1: 44;

 (r /. 1) = (r . 1) by A4, PARTFUN1:def 6

 .= ((( 1_. L) . (1 -' 1)) * (p . ((i + 1) -' 1))) by A3, A4

 .= ((( 1_. L) . (1 -' 1)) * (p . i)) by NAT_D: 34

 .= ((( 1_. L) . 0 ) * (p . i)) by XREAL_1: 232

 .= (( 1_ L) * (p . i)) by Th28

 .= (p . i);

 hence ((( 1_. L) *' p) . i) = (p . i) by A2, A11, A10, RLVECT_1: 4;

 end;

 hence thesis;

 end;

 Lm2:

 now

 let L be add-associative right_zeroed right_complementable well-unital Abelian distributive non empty doubleLoopStr;

 set Pm = ( Polynom-Ring L);

 let x,e be Element of Pm;

 reconsider p = x as Polynomial of L by Def10;

 assume

 A1: e = ( 1. Pm);



 A2: ( 1. Pm) = ( 1_. L) by Def10;



 hence (x * e) = (p *' ( 1_. L)) by A1, Def10

 .= x by Th33;



 thus (e * x) = (( 1_. L) *' p) by A1, A2, Def10

 .= x by Th33a;

 end;

 registration

 let L be add-associative right_zeroed right_complementable well-unital Abelian distributive non empty doubleLoopStr;

 cluster ( Polynom-Ring L) -> well-unital;

 coherence by Lm2;

 end

 registration

 let L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

 cluster ( Polynom-Ring L) -> distributive;

 coherence

 proof

 let p,q,r be Element of ( Polynom-Ring L);

 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 Th29

 .= ((p * q) + (p * r)) by A1, Def10;



 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 Th30

 .= ((q * p) + (r * p)) by A2, Def10;

 end;

 end

 theorem :: POLYNOM3:37

 for L be add-associative right_zeroed right_complementable well-unital Abelian distributive non empty doubleLoopStr holds ( 1. ( Polynom-Ring L)) = ( 1_. L) by Def10;