let o1, o2 be non empty Ordinal; :: thesis:
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis:
set P2 = Polynom-Ring ((o1 +^ o2),L);
set P1 = Polynom-Ring (o1,(Polynom-Ring (o2,L)));
defpred S₁[ set , set ] means for P being Polynomial of o1,(Polynom-Ring (o2,L)) st $1 = P holds
$2 = Compress P;
reconsider 1P1 = 1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider 1P2 = 1_ (Polynom-Ring ((o1 +^ o2),L)) as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;
A1: for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ex u being Element of (Polynom-Ring ((o1 +^ o2),L)) st S₁[x,u]

let x be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); :: thesis:
reconsider Q = x as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider u = Compress Q as Element of (Polynom-Ring ((o1 +^ o2),L)) by POLYNOM1:def 11;
take u ; :: thesis:
let P be Polynomial of o1,(Polynom-Ring (o2,L)); :: thesis:
assume x = P ; :: thesis:
hence u = Compress P ; :: thesis:

end;

consider f being Function of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L)) such that
A2: for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
reconsider f = f as Function of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))),(Polynom-Ring ((o1 +^ o2),L)) ;
take f ; :: according to QUOFIELD:def 23 :: thesis:
thus f is additive :: according to RINGCAT1:def 1,MOD_4:def 8,MOD_4:def 12 :: thesis: ,L))) )

proof

let x, y be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); :: according to VECTSP_1:def 19 :: thesis:
reconsider x9 = x, y9 = y as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ;
reconsider p = x9, q = y9 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider fp = f . x, fq = f . y, fpq = f . (x + y) as Element of (Polynom-Ring ((o1 +^ o2),L)) ;
reconsider fp = fp, fq = fq, fpq = fpq as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;
for x being bag of o1 +^ o2 holds fpq . x = (fp . x) + (fq . x)

proof

let b be bag of o1 +^ o2; :: thesis:
reconsider b9 = b as Element of Bags (o1 +^ o2) by PRE_POLY:def 12;
consider b1 being Element of Bags o1, b2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A3: Q1 = p . b1 and
A4: b9 = b1 +^ b2 and
A5: (Compress p) . b9 = Q1 . b2 by Def2;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q19 being Polynomial of o2,L such that
A6: Q19 = q . b19 and
A7: b9 = b19 +^ b29 and
A8: (Compress q) . b9 = Q19 . b29 by Def2;
consider b199 being Element of Bags o1, b299 being Element of Bags o2, Q199 being Polynomial of o2,L such that
A9: Q199 = (p + q) . b199 and
A10: b9 = b199 +^ b299 and
A11: (Compress (p + q)) . b9 = Q199 . b299 by Def2;
A12: b19 = b199 by A7, A10, Th7;
reconsider b1 = b1 as bag of o1 ;
A13: (p + q) . b1 = (p . b1) + (q . b1) by POLYNOM1:15;
b1 = b19 by A4, A7, Th7;
then Q199 = Q1 + Q19 by A3, A6, A9, A12, A13, POLYNOM1:def 11;
then A14: Q199 . b2 = (Q1 . b2) + (Q19 . b2) by POLYNOM1:15;
A15: b29 = b299 by A7, A10, Th7;
A16: b2 = b29 by A4, A7, Th7;
x + y = p + q by POLYNOM1:def 11;
hence fpq . b = (Compress (p + q)) . b9 by A2
.= ((Compress p) . b9) + (fq . b) by A2, A5, A8, A11, A16, A15, A14
.= (fp . b) + (fq . b) by A2 ;
:: thesis:

end;

hence f . (x + y) = fp + fq by POLYNOM1:16
.= (f . x) + (f . y) by POLYNOM1:def 11 ;
:: thesis:

end;

now :: thesis:

let x, y be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); :: thesis:
reconsider x9 = x, y9 = y as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ;
reconsider p = x9, q = y9 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider fp = f . x, fq = f . y as Element of (Polynom-Ring ((o1 +^ o2),L)) ;
reconsider fp = fp, fq = fq as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;
f . (x * y) = f . (p *' q) by POLYNOM1:def 11;
then reconsider fpq9 = f . (p *' q) as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;
A17: for b being bag of o1 +^ o2 ex s being FinSequence of the carrier of L st
( fpq9 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

proof

reconsider x = p *' q as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by POLYNOM1:def 11;
let c be bag of o1 +^ o2; :: thesis:
reconsider b = c as Element of Bags (o1 +^ o2) by PRE_POLY:def 12;
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A18: b = b1 +^ b2 by Th6;
reconsider b1 = b1 as bag of o1 ;
consider r being FinSequence of the carrier of (Polynom-Ring (o2,L)) such that
A19: (p *' q) . b1 = Sum r and
A20: len r = len (decomp b1) and
A21: for k being Element of NAT st k in dom r holds
ex a19, b19 being bag of o1 st
( (decomp b1) /. k = <*a19,b19*> & r /. k = (p . a19) * (q . b19) ) by POLYNOM1:def 10;
for x being object st x in dom r holds
r . x is Function

proof

let x be object ; :: thesis:
assume x in dom r ; :: thesis:
then A22: r . x in rng r by FUNCT_1:3;
rng r c= the carrier of (Polynom-Ring (o2,L)) by FINSEQ_1:def 4;
hence r . x is Function by A22, POLYNOM1:def 11; :: thesis:

end;

then reconsider rFF = r as Function-yielding Function by FUNCOP_1:def 6;
deffunc H₁( object ) -> set = (rFF . $1) . b2;
consider rFFb2 being Function such that
A23: dom rFFb2 = dom r and
A24: for i being object st i in dom r holds
rFFb2 . i = H₁(i) from FUNCT_1:sch 3();
ex i being Nat st dom r = Seg i by FINSEQ_1:def 2;
then reconsider rFFb2 = rFFb2 as FinSequence by A23, FINSEQ_1:def 2;
A25: rng rFFb2 c= the carrier of L

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
A26: rng rFF c= the carrier of (Polynom-Ring (o2,L)) by FINSEQ_1:def 4;
assume u in rng rFFb2 ; :: thesis:
then consider x being object such that
A27: x in dom rFFb2 and
A28: u = rFFb2 . x by FUNCT_1:def 3;
rFF . x in rng rFF by A23, A27, FUNCT_1:3;
then A29: rFF . x is Function of (Bags o2), the carrier of L by A26, POLYNOM1:def 11;
then A30: rng (rFF . x) c= the carrier of L by RELAT_1:def 19;
dom (rFF . x) = Bags o2 by A29, FUNCT_2:def 1;
then A31: (rFF . x) . b2 in rng (rFF . x) by FUNCT_1:3;
rFFb2 . x = (rFF . x) . b2 by A23, A24, A27;
hence u in the carrier of L by A28, A30, A31; :: thesis:

end;

defpred S₂[ set , set ] means ex a19, b19 being bag of o1 ex Fk being FinSequence of the carrier of L ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = $2 & (decomp b1) /. $1 = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) );
A32: for k being Nat st k in Seg (len r) holds
ex x being Element of the carrier of L * st S₂[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len r) ; :: thesis:
then k in dom (decomp b1) by A20, FINSEQ_1:def 3;
then consider a19, b19 being bag of o1 such that
A33: (decomp b1) /. k = <*a19,b19*> and
b1 = a19 + b19 by PRE_POLY:68;
reconsider pa199 = p . a19, qb199 = q . b19 as Element of (Polynom-Ring (o2,L)) ;
reconsider pa19 = pa199, qb19 = qb199 as Polynomial of o2,L by POLYNOM1:def 11;
defpred S₃[ set , set ] means ex a199, b199 being bag of o2 st
( (decomp b2) /. $1 = <*a199,b199*> & $2 = (pa19 . a199) * (qb19 . b199) );
A34: for k being Nat st k in Seg (len (decomp b2)) holds
ex x being Element of L st S₃[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len (decomp b2)) ; :: thesis:
then k in dom (decomp b2) by FINSEQ_1:def 3;
then consider a199, b199 being bag of o2 such that
A35: (decomp b2) /. k = <*a199,b199*> and
b2 = a199 + b199 by PRE_POLY:68;
reconsider x = (pa19 . a199) * (qb19 . b199) as Element of L ;
take x ; :: thesis:
take a199 ; :: thesis:
take b199 ; :: thesis:
thus ( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) ) by A35; :: thesis:

end;

consider Fk being FinSequence of the carrier of L such that
A36: dom Fk = Seg (len (decomp b2)) and
A37: for k being Nat st k in Seg (len (decomp b2)) holds
S₃[k,Fk /. k] from RECDEF_1:sch 17(A34);
reconsider x = Fk as Element of the carrier of L * by FINSEQ_1:def 11;
take x ; :: thesis:
take a19 ; :: thesis:
take b19 ; :: thesis:
take Fk ; :: thesis:
take pa19 ; :: thesis:
take qb19 ; :: thesis:
thus ( pa19 = p . a19 & qb19 = q . b19 & Fk = x ) ; :: thesis:
thus (decomp b1) /. k = <*a19,b19*> by A33; :: thesis:
thus len Fk = len (decomp b2) by A36, FINSEQ_1:def 3; :: thesis:
let m be Nat; :: thesis:
assume m in dom Fk ; :: thesis:
hence ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) by A36, A37; :: thesis:

end;

consider F being FinSequence of the carrier of L * such that
A38: dom F = Seg (len r) and
A39: for k being Nat st k in Seg (len r) holds
S₂[k,F /. k] from RECDEF_1:sch 17(A32);
take s = FlattenSeq F; :: thesis:
A40: len (Sum F) = len F by MATRLIN:def 6;
reconsider rFFb2 = rFFb2 as FinSequence of the carrier of L by A25, FINSEQ_1:def 4;
A41: f . x = Compress (p *' q) by A2;
A42: dom rFFb2 = dom F by A38, A23, FINSEQ_1:def 3
.= dom (Sum F) by A40, FINSEQ_3:29 ;
for k being Nat st k in dom rFFb2 holds
rFFb2 . k = (Sum F) . k

proof

let k be Nat; :: thesis:
assume A43: k in dom rFFb2 ; :: thesis:
consider c1, d1 being bag of o1 such that
A44: (decomp b1) /. k = <*c1,d1*> and
A45: r /. k = (p . c1) * (q . d1) by A21, A23, A43;
k in Seg (len r) by A23, A43, FINSEQ_1:def 3;
then consider a19, b19 being bag of o1, Fk being FinSequence of the carrier of L, pa19, qb19 being Polynomial of o2,L such that
A46: ( pa19 = p . a19 & qb19 = q . b19 ) and
A47: Fk = F /. k and
A48: (decomp b1) /. k = <*a19,b19*> and
A49: len Fk = len (decomp b2) and
A50: for ki being Nat st ki in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. ki = <*a199,b199*> & Fk /. ki = (pa19 . a199) * (qb19 . b199) ) by A39;
A51: ( c1 = a19 & d1 = b19 ) by A44, A48, FINSEQ_1:77;
consider s1 being FinSequence of the carrier of L such that
A52: (pa19 *' qb19) . b2 = Sum s1 and
A53: len s1 = len (decomp b2) and
A54: for ki being Element of NAT st ki in dom s1 holds
ex x1, y2 being bag of o2 st
( (decomp b2) /. ki = <*x1,y2*> & s1 /. ki = (pa19 . x1) * (qb19 . y2) ) by POLYNOM1:def 10;
A55: dom s1 = Seg (len s1) by FINSEQ_1:def 3;

now :: thesis:

let ki be Nat; :: thesis:
assume A56: ki in dom s1 ; :: thesis:
then A57: s1 /. ki = s1 . ki by PARTFUN1:def 6;
A58: ki in dom Fk by A49, A53, A55, A56, FINSEQ_1:def 3;
then consider a199, b199 being bag of o2 such that
A59: (decomp b2) /. ki = <*a199,b199*> and
A60: Fk /. ki = (pa19 . a199) * (qb19 . b199) by A50;
consider x1, y2 being bag of o2 such that
A61: (decomp b2) /. ki = <*x1,y2*> and
A62: s1 /. ki = (pa19 . x1) * (qb19 . y2) by A54, A56;
( x1 = a199 & y2 = b199 ) by A61, A59, FINSEQ_1:77;
hence s1 . ki = Fk . ki by A62, A58, A60, A57, PARTFUN1:def 6; :: thesis:

end;

then A63: s1 = Fk by A49, A53, FINSEQ_2:9;
A64: rFF . k = r /. k by A23, A43, PARTFUN1:def 6
.= pa19 *' qb19 by A45, A46, A51, POLYNOM1:def 11 ;
thus rFFb2 . k = (rFF . k) . b2 by A23, A24, A43
.= (Sum F) /. k by A42, A43, A47, A64, A52, A63, MATRLIN:def 6
.= (Sum F) . k by A42, A43, PARTFUN1:def 6 ; :: thesis:

end;

then A65: rFFb2 = Sum F by A42;
reconsider Sr = Sum r as Polynomial of o2,L by POLYNOM1:def 11;
consider gg being sequence of the carrier of (Polynom-Ring (o2,L)) such that
A66: Sum r = gg . (len r) and
A67: gg . 0 = 0. (Polynom-Ring (o2,L)) and
A68: for j being Nat
for v being Element of (Polynom-Ring (o2,L)) st j < len r & v = r . (j + 1) holds
gg . (j + 1) = (gg . j) + v by RLVECT_1:def 12;
defpred S₃[ Nat, set ] means for pp being Polynomial of o2,L st $1 <= len r & pp = gg . $1 holds
$2 = pp . b2;
A69: for x being Element of NAT ex y being Element of L st S₃[x,y]

proof

let x be Element of NAT ; :: thesis:
reconsider pp9 = gg . x as Polynomial of o2,L by POLYNOM1:def 11;
take y = pp9 . b2; :: thesis:
let pp be Polynomial of o2,L; :: thesis:
assume that
x <= len r and
A70: pp = gg . x ; :: thesis:
thus y = pp . b2 by A70; :: thesis:

end;

consider ff being sequence of the carrier of L such that
A71: for j being Element of NAT holds S₃[j,ff . j] from FUNCT_2:sch 3(A69);
A72: for j being Nat holds S₃[j,ff . j]

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence S₃[n,ff . n] by A71; :: thesis:

end;

defpred S₄[ set , set ] means ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = $2 & (decomp b1) /. $1 = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) );
A73: for i being Nat st i in Seg (len r) holds
ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S₄[i,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len r) ; :: thesis:
then k in dom (decomp b1) by A20, FINSEQ_1:def 3;
then consider a19, b19 being bag of o1 such that
A74: (decomp b1) /. k = <*a19,b19*> and
b1 = a19 + b19 by PRE_POLY:68;
reconsider a19 = a19, b19 = b19 as Element of Bags o1 by PRE_POLY:def 12;
defpred S₅[ set , set ] means ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. $1 = <*a199,b199*> & $2 = <*(a19 +^ a199),(b19 +^ b199)*> );
A75: for k being Nat st k in Seg (len (decomp b2)) holds
ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S₅[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len (decomp b2)) ; :: thesis:
then k in dom (decomp b2) by FINSEQ_1:def 3;
then consider a199, b199 being bag of o2 such that
A76: (decomp b2) /. k = <*a199,b199*> and
b2 = a199 + b199 by PRE_POLY:68;
reconsider a199 = a199, b199 = b199 as Element of Bags o2 by PRE_POLY:def 12;
reconsider x = <*(a19 +^ a199),(b19 +^ b199)*> as Element of 2 -tuples_on (Bags (o1 +^ o2)) ;
take x ; :: thesis:
take a199 ; :: thesis:
take b199 ; :: thesis:
thus ( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> ) by A76; :: thesis:

end;

consider Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
A77: dom Fk = Seg (len (decomp b2)) and
A78: for k being Nat st k in Seg (len (decomp b2)) holds
S₅[k,Fk /. k] from RECDEF_1:sch 17(A75);
reconsider x = Fk as Element of (2 -tuples_on (Bags (o1 +^ o2))) * by FINSEQ_1:def 11;
take x ; :: thesis:
take a19 ; :: thesis:
take b19 ; :: thesis:
take Fk ; :: thesis:
thus Fk = x ; :: thesis:
thus (decomp b1) /. k = <*a19,b19*> by A74; :: thesis:
thus len Fk = len (decomp b2) by A77, FINSEQ_1:def 3; :: thesis:
let m be Nat; :: thesis:
assume m in dom Fk ; :: thesis:
hence ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) by A77, A78; :: thesis:

end;

consider G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * such that
A79: dom G = Seg (len r) and
A80: for i being Nat st i in Seg (len r) holds
S₄[i,G /. i] from RECDEF_1:sch 17(A73);
A81: for i being Nat st i in Seg (len r) holds
S₄[i,G /. i] by A80;
A82: dom (Card F) = dom F by CARD_3:def 2;
A83: for j being Nat st j in dom (Card F) holds
(Card F) . j = (Card G) . j

proof

let j be Nat; :: thesis:
assume A84: j in dom (Card F) ; :: thesis:
then A85: j in dom F by CARD_3:def 2;
then A86: (Card F) . j = card (F . j) by CARD_3:def 2;
A87: ( ex a19, b19 being bag of o1 ex Fk being FinSequence of the carrier of L ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = F /. j & (decomp b1) /. j = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) ) & ex a29, b29 being Element of Bags o1 ex Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Gk = G /. j & (decomp b1) /. j = <*a29,b29*> & len Gk = len (decomp b2) & ( for m being Nat st m in dom Gk holds
ex a299, b299 being Element of Bags o2 st
( (decomp b2) /. m = <*a299,b299*> & Gk /. m = <*(a29 +^ a299),(b29 +^ b299)*> ) ) ) ) by A38, A39, A80, A85;
card (F . j) = card (F /. j) by A85, PARTFUN1:def 6
.= card (G . j) by A38, A79, A82, A84, A87, PARTFUN1:def 6 ;
hence (Card F) . j = (Card G) . j by A38, A79, A82, A84, A86, CARD_3:def 2; :: thesis:

end;

consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A88: Q1 = (p *' q) . c1 and
A89: b = c1 +^ c2 and
A90: (Compress (p *' q)) . b = Q1 . c2 by Def2;
A91: c1 = b1 by A18, A89, Th7;
then dom G = dom (decomp c1) by A20, A79, FINSEQ_1:def 3;
then A92: decomp c = FlattenSeq G by A18, A79, A81, A91, Th14;
A93: for j being Nat
for v being Element of L st j < len rFFb2 & v = rFFb2 . (j + 1) holds
ff . (j + 1) = (ff . j) + v

proof

let j be Nat; :: thesis:
let v be Element of L; :: thesis:
assume that
A94: j < len rFFb2 and
A95: v = rFFb2 . (j + 1) ; :: thesis:
reconsider w = r /. (j + 1), pp = gg . j, pp9 = gg . (j + 1) as Polynomial of o2,L by POLYNOM1:def 11;
reconsider w1 = w, pp1 = pp, pp19 = pp9 as Element of (Polynom-Ring (o2,L)) ;
reconsider w1 = w1, pp1 = pp1, pp19 = pp19 as Element of (Polynom-Ring (o2,L)) ;
A96: j < len r by A23, A94, FINSEQ_3:29;
then A97: j + 1 <= len r by NAT_1:13;
then A98: w = r . (j + 1) by FINSEQ_4:15, NAT_1:11;
then A99: pp19 = pp1 + w1 by A68, A96;
1 <= j + 1 by NAT_1:11;
then j + 1 in dom r by A97, FINSEQ_3:25;
then A100: w . b2 = v by A24, A95, A98;
j + 1 <= len r by A96, NAT_1:13;
hence ff . (j + 1) = pp9 . b2 by A72
.= (pp + w) . b2 by A99, POLYNOM1:def 11
.= (pp . b2) + (w . b2) by POLYNOM1:15
.= (ff . j) + v by A72, A96, A100 ;
:: thesis:

end;

gg . 0 = 0_ (o2,L) by A67, POLYNOM1:def 11;
then A101: ff . 0 = (0_ (o2,L)) . b2 by A72, NAT_1:2
.= 0. L by POLYNOM1:22 ;
len rFFb2 = len r by A23, FINSEQ_3:29;
then Sr . b2 = ff . (len rFFb2) by A66, A72;
then A102: Sr . b2 = Sum rFFb2 by A101, A93, RLVECT_1:def 12;
( b1 = c1 & b2 = c2 ) by A18, A89, Th7;
hence fpq9 . c = Sum s by A19, A88, A90, A65, A102, A41, POLYNOM1:14; :: thesis:
dom (Card G) = dom G by CARD_3:def 2;
then len (Card F) = len (Card G) by A38, A79, A82, FINSEQ_3:29;
then A103: Card F = Card G by A83, FINSEQ_2:9;
hence A104: len s = len (decomp c) by A92, PRE_POLY:28; :: thesis:
let k be Element of NAT ; :: thesis:
assume A105: k in dom s ; :: thesis:
then consider i, j being Nat such that
A106: i in dom F and
A107: j in dom (F . i) and
A108: k = (Sum (Card (F | (i -' 1)))) + j and
A109: (F . i) . j = (FlattenSeq F) . k by PRE_POLY:29;
A110: k in dom (decomp c) by A104, A105, FINSEQ_3:29;
then consider i9, j9 being Nat such that
A111: i9 in dom G and
A112: j9 in dom (G . i9) and
A113: k = (Sum (Card (G | (i9 -' 1)))) + j9 and
A114: (G . i9) . j9 = (decomp c) . k by A92, PRE_POLY:29;
(Sum ((Card F) | (i -' 1))) + j = (Sum (Card (F | (i -' 1)))) + j by POLYNOM3:16
.= (Sum ((Card G) | (i9 -' 1))) + j9 by A108, A113, POLYNOM3:16 ;
then A115: ( i = i9 & j = j9 ) by A103, A106, A107, A111, A112, POLYNOM3:22;
consider c1, c2 being bag of o1 +^ o2 such that
A116: (decomp c) /. k = <*c1,c2*> and
c = c1 + c2 by A110, PRE_POLY:68;
reconsider cc1 = c1, cc2 = c2 as Element of Bags (o1 +^ o2) by PRE_POLY:def 12;
consider cb1 being Element of Bags o1, cb2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A117: Q1 = p . cb1 and
A118: cc1 = cb1 +^ cb2 and
A119: (Compress p) . cc1 = Q1 . cb2 by Def2;
consider a19, b19 being bag of o1, Fk being FinSequence of the carrier of L, pa19, qb19 being Polynomial of o2,L such that
A120: pa19 = p . a19 and
A121: qb19 = q . b19 and
A122: Fk = F /. i and
A123: (decomp b1) /. i = <*a19,b19*> and
len Fk = len (decomp b2) and
A124: for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) by A38, A39, A106;
consider ga19, gb19 being Element of Bags o1, Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
A125: Gk = G /. i and
A126: (decomp b1) /. i = <*ga19,gb19*> and
len Gk = len (decomp b2) and
A127: for m being Nat st m in dom Gk holds
ex ga199, gb199 being Element of Bags o2 st
( (decomp b2) /. m = <*ga199,gb199*> & Gk /. m = <*(ga19 +^ ga199),(gb19 +^ gb199)*> ) by A38, A80, A106;
A128: b19 = gb19 by A123, A126, FINSEQ_1:77;
A129: Gk = G . i by A38, A79, A106, A125, PARTFUN1:def 6;
then consider ga199, gb199 being Element of Bags o2 such that
A130: (decomp b2) /. j = <*ga199,gb199*> and
A131: Gk /. j = <*(ga19 +^ ga199),(gb19 +^ gb199)*> by A112, A115, A127;
A132: <*c1,c2*> = (G . i) . j by A110, A116, A114, A115, PARTFUN1:def 6
.= <*(ga19 +^ ga199),(gb19 +^ gb199)*> by A112, A115, A129, A131, PARTFUN1:def 6 ;
then c1 = ga19 +^ ga199 by FINSEQ_1:77;
then A133: ( cb1 = ga19 & cb2 = ga199 ) by A118, Th7;
A134: a19 = ga19 by A123, A126, FINSEQ_1:77;
j in dom Fk by A106, A107, A122, PARTFUN1:def 6;
then consider a199, b199 being bag of o2 such that
A135: (decomp b2) /. j = <*a199,b199*> and
A136: Fk /. j = (pa19 . a199) * (qb19 . b199) by A124;
a199 = ga199 by A130, A135, FINSEQ_1:77;
then A137: pa19 . a199 = fp . c1 by A2, A120, A117, A119, A133, A134;
take c1 ; :: thesis:
take c2 ; :: thesis:
thus (decomp c) /. k = <*c1,c2*> by A116; :: thesis:
consider cb1 being Element of Bags o1, cb2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A138: Q1 = q . cb1 and
A139: cc2 = cb1 +^ cb2 and
A140: (Compress q) . cc2 = Q1 . cb2 by Def2;
c2 = gb19 +^ gb199 by A132, FINSEQ_1:77;
then A141: ( cb1 = gb19 & cb2 = gb199 ) by A139, Th7;
A142: Fk = F . i by A106, A122, PARTFUN1:def 6;
b199 = gb199 by A130, A135, FINSEQ_1:77;
then A143: qb19 . b199 = fq . c2 by A2, A121, A128, A138, A140, A141;
thus s /. k = s . k by A105, PARTFUN1:def 6
.= (fp . c1) * (fq . c2) by A107, A109, A142, A136, A137, A143, PARTFUN1:def 6 ; :: thesis:

end;

thus f . (x * y) = f . (p *' q) by POLYNOM1:def 11
.= fp *' fq by A17, POLYNOM1:def 10
.= (f . x) * (f . y) by POLYNOM1:def 11 ; :: thesis:

end;

hence f is multiplicative by GROUP_6:def 6; :: thesis: ,L))) )
A144: for b being Element of Bags (o1 +^ o2) holds (Compress 1P1) . b = 1P2 . b

proof

let b be Element of Bags (o1 +^ o2); :: thesis:
A145: 1P2 . b = (1_ ((o1 +^ o2),L)) . b by POLYNOM1:31;
consider b1 being Element of Bags o1, b2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A146: Q1 = 1P1 . b1 and
A147: b = b1 +^ b2 and
A148: (Compress 1P1) . b = Q1 . b2 by Def2;

per cases ;

suppose A149: b = EmptyBag (o1 +^ o2) ; :: thesis:

then A150: b1 = EmptyBag o1 by A147, Th5;
A151: b2 = EmptyBag o2 by A147, A149, Th5;
Q1 = (1_ (o1,(Polynom-Ring (o2,L)))) . b1 by A146, POLYNOM1:31
.= 1_ (Polynom-Ring (o2,L)) by A150, POLYNOM1:25 ;
then Q1 . b2 = (1_ (o2,L)) . b2 by POLYNOM1:31
.= 1_ L by A151, POLYNOM1:25
.= 1P2 . b by A145, A149, POLYNOM1:25 ;
hence (Compress 1P1) . b = 1P2 . b by A148; :: thesis:

end;

suppose A152: b <> EmptyBag (o1 +^ o2) ; :: thesis:

then A153: ( b1 <> EmptyBag o1 or b2 <> EmptyBag o2 ) by A147, Th5;

now :: thesis:

per cases ;

suppose A154: b1 = EmptyBag o1 ; :: thesis:

Q1 = (1_ (o1,(Polynom-Ring (o2,L)))) . b1 by A146, POLYNOM1:31
.= 1_ (Polynom-Ring (o2,L)) by A154, POLYNOM1:25
.= 1_ (o2,L) by POLYNOM1:31 ;
then Q1 . b2 = 0. L by A153, A154, POLYNOM1:25
.= 1P2 . b by A145, A152, POLYNOM1:25 ;
hence (Compress 1P1) . b = 1P2 . b by A148; :: thesis:

end;

suppose A155: b1 <> EmptyBag o1 ; :: thesis:

Q1 = (1_ (o1,(Polynom-Ring (o2,L)))) . b1 by A146, POLYNOM1:31
.= 0. (Polynom-Ring (o2,L)) by A155, POLYNOM1:25
.= 0_ (o2,L) by POLYNOM1:def 11 ;
then Q1 . b2 = 0. L by POLYNOM1:22
.= 1P2 . b by A145, A152, POLYNOM1:25 ;
hence (Compress 1P1) . b = 1P2 . b by A148; :: thesis:

end;

hence (Compress 1P1) . b = 1P2 . b ; :: thesis:

end;

f . (1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L))))) = Compress 1P1 by A2
.= 1_ (Polynom-Ring ((o1 +^ o2),L)) by A144, FUNCT_2:63 ;
hence f is unity-preserving by GROUP_1:def 13; :: thesis: ,L))) )
thus f is one-to-one :: thesis: ,L)))

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume x1 in dom f ; :: thesis:
then reconsider x19 = x1 as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def 1;
assume x2 in dom f ; :: thesis:
then reconsider x29 = x2 as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def 1;
reconsider x299 = x29 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider x199 = x19 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
A156: f . x29 = Compress x299 by A2;
then reconsider w2 = f . x29 as Polynomial of (o1 +^ o2),L ;
A157: f . x19 = Compress x199 by A2;
then reconsider w1 = f . x19 as Polynomial of (o1 +^ o2),L ;
assume A158: f . x1 = f . x2 ; :: thesis:

now :: thesis:

let b1 be Element of Bags o1; :: thesis:
reconsider x199b1 = x199 . b1, x299b1 = x299 . b1 as Polynomial of o2,L by POLYNOM1:def 11;

now :: thesis:

let b2 be Element of Bags o2; :: thesis:
set b = b1 +^ b2;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A159: Q1 = x199 . b19 and
A160: b1 +^ b2 = b19 +^ b29 and
A161: w1 . (b1 +^ b2) = Q1 . b29 by A157, Def2;
A162: ( b1 = b19 & b2 = b29 ) by A160, Th7;
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q19 being Polynomial of o2,L such that
A163: Q19 = x299 . c1 and
A164: b1 +^ b2 = c1 +^ c2 and
A165: w2 . (b1 +^ b2) = Q19 . c2 by A156, Def2;
b1 = c1 by A164, Th7;
hence x199b1 . b2 = x299b1 . b2 by A158, A159, A161, A163, A164, A165, A162, Th7; :: thesis:

end;

hence x199 . b1 = x299 . b1 by FUNCT_2:63; :: thesis:

end;

hence x1 = x2 by FUNCT_2:63; :: thesis:

end;

thus rng f c= the carrier of (Polynom-Ring ((o1 +^ o2),L)) by RELAT_1:def 19; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis:
thus the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= rng f :: thesis:

proof

defpred S₂[ set , set ] means ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 st
( $1 = b1 +^ b2 & $2 = b1 );
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) ; :: thesis:
then reconsider s = y as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;
defpred S₃[ Element of Bags o1, Element of (Polynom-Ring (o2,L))] means ex h being Function st
( h = $2 & ( for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = $1 +^ b2 holds
h . b2 = s . b ) );
A166: for x being Element of Bags (o1 +^ o2) ex y being Element of Bags o1 st S₂[x,y]

proof

let x be Element of Bags (o1 +^ o2); :: thesis:
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A167: x = b1 +^ b2 by Th6;
reconsider y = b1 as Element of Bags o1 ;
take y ; :: thesis:
take b1 ; :: thesis:
take b2 ; :: thesis:
thus x = b1 +^ b2 by A167; :: thesis:
thus y = b1 ; :: thesis:

end;

consider kk being Function of (Bags (o1 +^ o2)),(Bags o1) such that
A168: for b being Element of Bags (o1 +^ o2) holds S₂[b,kk . b] from FUNCT_2:sch 3(A166);
A169: for x being Element of Bags o1 ex y being Element of (Polynom-Ring (o2,L)) st S₃[x,y]

proof

defpred S₄[ set , set ] means ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 st
( $1 = b1 +^ b2 & $2 = b2 );
let x be Element of Bags o1; :: thesis:
reconsider b1 = x as Element of Bags o1 ;
defpred S₅[ Element of Bags o2, Element of L] means for b being Element of Bags (o1 +^ o2) st b = b1 +^ $1 holds
$2 = s . b;
A170: for p being Element of Bags o2 ex q being Element of L st S₅[p,q]

proof

let p be Element of Bags o2; :: thesis:
take s . (b1 +^ p) ; :: thesis:
let b be Element of Bags (o1 +^ o2); :: thesis:
assume b = b1 +^ p ; :: thesis:
hence s . (b1 +^ p) = s . b ; :: thesis:

end;

consider t being Function of (Bags o2), the carrier of L such that
A171: for b2 being Element of Bags o2 holds S₅[b2,t . b2] from FUNCT_2:sch 3(A170);
reconsider t = t as Function of (Bags o2),L ;
A172: for x being Element of Bags (o1 +^ o2) ex y being Element of Bags o2 st S₄[x,y]

proof

let x be Element of Bags (o1 +^ o2); :: thesis:
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A173: x = b1 +^ b2 by Th6;
reconsider y = b2 as Element of Bags o2 ;
take y ; :: thesis:
take b1 ; :: thesis:
take b2 ; :: thesis:
thus x = b1 +^ b2 by A173; :: thesis:
thus y = b2 ; :: thesis:

end;

consider kk being Function of (Bags (o1 +^ o2)),(Bags o2) such that
A174: for b being Element of Bags (o1 +^ o2) holds S₄[b,kk . b] from FUNCT_2:sch 3(A172);
Support t c= kk .: (Support s)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A175: x in Support t ; :: thesis:
then reconsider b2 = x as Element of Bags o2 ;
set b = b1 +^ b2;
t . x <> 0. L by A175, POLYNOM1:def 4;
then s . (b1 +^ b2) <> 0. L by A171;
then A176: ( dom kk = Bags (o1 +^ o2) & b1 +^ b2 in Support s ) by FUNCT_2:def 1, POLYNOM1:def 4;
ex b19 being Element of Bags o1 ex b29 being Element of Bags o2 st
( b1 +^ b2 = b19 +^ b29 & kk . (b1 +^ b2) = b29 ) by A174;
then x = kk . (b1 +^ b2) by Th7;
hence x in kk .: (Support s) by A176, FUNCT_1:def 6; :: thesis:

end;

then t is Polynomial of o2,L by POLYNOM1:def 5;
then reconsider t99 = t as Element of (Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider t9 = t as Function ;
take t99 ; :: thesis:
take t9 ; :: thesis:
thus t99 = t9 ; :: thesis:
let b2 be Element of Bags o2; :: thesis:
let b be Element of Bags (o1 +^ o2); :: thesis:
assume b = x +^ b2 ; :: thesis:
hence t9 . b2 = s . b by A171; :: thesis:

end;

consider g being Function of (Bags o1), the carrier of (Polynom-Ring (o2,L)) such that
A177: for x being Element of Bags o1 holds S₃[x,g . x] from FUNCT_2:sch 3(A169);
reconsider g = g as Function of (Bags o1),(Polynom-Ring (o2,L)) ;
A178: Support g c= kk .: (Support s)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A179: x in Support g ; :: thesis:
then reconsider b1 = x as Element of Bags o1 ;
consider h being Function such that
A180: h = g . b1 and
A181: for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = b1 +^ b2 holds
h . b2 = s . b by A177;
reconsider h = h as Polynomial of o2,L by A180, POLYNOM1:def 11;
g . b1 <> 0. (Polynom-Ring (o2,L)) by A179, POLYNOM1:def 4;
then g . b1 <> 0_ (o2,L) by POLYNOM1:def 11;
then consider b2 being Element of Bags o2 such that
A182: b2 in Support h by A180, POLYNOM2:17, SUBSET_1:4;
set b = b1 +^ b2;
h . b2 <> 0. L by A182, POLYNOM1:def 4;
then s . (b1 +^ b2) <> 0. L by A181;
then A183: ( dom kk = Bags (o1 +^ o2) & b1 +^ b2 in Support s ) by FUNCT_2:def 1, POLYNOM1:def 4;
ex b19 being Element of Bags o1 ex b29 being Element of Bags o2 st
( b1 +^ b2 = b19 +^ b29 & kk . (b1 +^ b2) = b19 ) by A168;
then x = kk . (b1 +^ b2) by Th7;
hence x in kk .: (Support s) by A183, FUNCT_1:def 6; :: thesis:

end;

then g is Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 5;
then reconsider g = g as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by POLYNOM1:def 11;
reconsider g9 = g as Polynomial of o1,(Polynom-Ring (o2,L)) by A178, POLYNOM1:def 5;

now :: thesis:

let b be Element of Bags (o1 +^ o2); :: thesis:
consider b1 being Element of Bags o1, b2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A184: ( Q1 = g9 . b1 & b = b1 +^ b2 & (Compress g9) . b = Q1 . b2 ) by Def2;
ex h being Function st
( h = g9 . b1 & ( for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = b1 +^ b2 holds
h . b2 = s . b ) ) by A177;
hence s . b = (Compress g9) . b by A184; :: thesis:

end;

then A185: y = Compress g9 by FUNCT_2:63
.= f . g by A2 ;
dom f = the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def 1;
hence y in rng f by A185, FUNCT_1:3; :: thesis:

end;