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 27;
reconsider 1P2 = 1_ (Polynom-Ring (o1 +^ o2),L) as Polynomial of (o1 +^ o2),L by POLYNOM1:def 27;
A1: for x being Element of ex u being Element of st S₁[x,u]

let x be Element of ; :: thesis:
reconsider Q = x as Polynomial of o1, Polynom-Ring o2,L by POLYNOM1:def 27;
reconsider u = Compress Q as Element of by POLYNOM1:def 27;
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 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 26 :: thesis:
thus A3: f is additive :: according to QUOFIELD:def 21,QUOFIELD:def 23,QUOFIELD:def 24 :: thesis:

proof

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

proof

let b be bag of o1 +^ o2; :: thesis:
reconsider b' = 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
A4: Q1 = p . b1 and
A5: b' = b1 +^ b2 and
A6: (Compress p) . b' = Q1 . b2 by Def2;
consider b1' being Element of Bags o1, b2' being Element of Bags o2, Q1' being Polynomial of o2,L such that
A7: Q1' = q . b1' and
A8: b' = b1' +^ b2' and
A9: (Compress q) . b' = Q1' . b2' by Def2;
consider b1'' being Element of Bags o1, b2'' being Element of Bags o2, Q1'' being Polynomial of o2,L such that
A10: Q1'' = (p + q) . b1'' and
A11: b' = b1'' +^ b2'' and
A12: (Compress (p + q)) . b' = Q1'' . b2'' by Def2;
A13: b1' = b1'' by A8, A11, Th7;
reconsider b1 = b1 as bag of o1 ;
A14: (p + q) . b1 = (p . b1) + (q . b1) by POLYNOM1:def 21;
b1 = b1' by A5, A8, Th7;
then Q1'' = Q1 + Q1' by A4, A7, A10, A13, A14, POLYNOM1:def 27;
then A15: Q1'' . b2 = (Q1 . b2) + (Q1' . b2) by POLYNOM1:def 21;
A16: b2' = b2'' by A8, A11, Th7;
A17: b2 = b2' by A5, A8, Th7;
x + y = p + q by POLYNOM1:def 27;
hence fpq . b = (Compress (p + q)) . b' by A2
.= ((Compress p) . b') + (fq . b) by A2, A6, A9, A12, A17, A16, A15
.= (fp . b) + (fq . b) by A2 ;
:: thesis:

end;

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

end;

now

let x, y be Element of ; :: thesis:
reconsider x' = x, y' = y as Element of ;
reconsider p = x', q = y' as Polynomial of o1, Polynom-Ring o2,L by POLYNOM1:def 27;
reconsider fp = f . x, fq = f . y as Element of ;
reconsider fp = fp, fq = fq as Polynomial of (o1 +^ o2),L by POLYNOM1:def 27;
f . (x * y) = f . (p *' q) by POLYNOM1:def 27;
then reconsider fpq' = f . (p *' q) as Polynomial of (o1 +^ o2),L by POLYNOM1:def 27;
A18: for b being bag of o1 +^ o2 ex s being FinSequence of the carrier of L st
( fpq' . 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 by POLYNOM1:def 27;
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
A19: 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
A20: (p *' q) . b1 = Sum r and
A21: len r = len (decomp b1) and
A22: for k being Element of NAT st k in dom r holds
ex a1', b1' being bag of o1 st
( (decomp b1) /. k = <*a1',b1'*> & r /. k = (p . a1') * (q . b1') ) by POLYNOM1:def 26;
for x being set st x in dom r holds
r . x is Function

proof

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

end;

then reconsider rFF = r as Function-yielding Function by FUNCOP_1:def 6;
deffunc H₁( set ) -> set = (rFF . $1) . b2;
consider rFFb2 being Function such that
A24: dom rFFb2 = dom r and
A25: for i being set 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 A24, FINSEQ_1:def 2;
A26: rng rFFb2 c= the carrier of L

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
A27: 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 set such that
A28: x in dom rFFb2 and
A29: u = rFFb2 . x by FUNCT_1:def 5;
rFF . x in rng rFF by A24, A28, FUNCT_1:12;
then A30: rFF . x is Function of Bags o2,the carrier of L by A27, POLYNOM1:def 27;
then A31: rng (rFF . x) c= the carrier of L by RELAT_1:def 19;
dom (rFF . x) = Bags o2 by A30, FUNCT_2:def 1;
then A32: (rFF . x) . b2 in rng (rFF . x) by FUNCT_1:12;
rFFb2 . x = (rFF . x) . b2 by A24, A25, A28;
hence u in the carrier of L by A29, A31, A32; :: thesis:

end;

defpred S₂[ set , set ] means ex a1', b1' being bag of o1 ex Fk being FinSequence of the carrier of L ex pa1', qb1' being Polynomial of o2,L st
( pa1' = p . a1' & qb1' = q . b1' & Fk = $2 & (decomp b1) /. $1 = <*a1',b1'*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a1'', b1'' being bag of o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) ) );
A33: for k being Element of 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 Element of NAT ; :: thesis:
assume k in Seg (len r) ; :: thesis:
then k in dom (decomp b1) by A21, FINSEQ_1:def 3;
then consider a1', b1' being bag of o1 such that
A34: (decomp b1) /. k = <*a1',b1'*> and
b1 = a1' + b1' by PRE_POLY:68;
reconsider pa1'' = p . a1', qb1'' = q . b1' as Element of ;
reconsider pa1' = pa1'', qb1' = qb1'' as Polynomial of o2,L by POLYNOM1:def 27;
defpred S₃[ set , set ] means ex a1'', b1'' being bag of o2 st
( (decomp b2) /. $1 = <*a1'',b1''*> & $2 = (pa1' . a1'') * (qb1' . b1'') );
A35: for k being Element of NAT st k in Seg (len (decomp b2)) holds
ex x being Element of st S₃[k,x]

proof

let k be Element of NAT ; :: thesis:
assume k in Seg (len (decomp b2)) ; :: thesis:
then k in dom (decomp b2) by FINSEQ_1:def 3;
then consider a1'', b1'' being bag of o2 such that
A36: (decomp b2) /. k = <*a1'',b1''*> and
b2 = a1'' + b1'' by PRE_POLY:68;
reconsider x = (pa1' . a1'') * (qb1' . b1'') as Element of ;
take x ; :: thesis:
take a1'' ; :: thesis:
take b1'' ; :: thesis:
thus ( (decomp b2) /. k = <*a1'',b1''*> & x = (pa1' . a1'') * (qb1' . b1'') ) by A36; :: thesis:

end;

consider Fk being FinSequence of the carrier of L such that
A37: dom Fk = Seg (len (decomp b2)) and
A38: for k being Element of NAT st k in Seg (len (decomp b2)) holds
S₃[k,Fk /. k] from POLYNOM2:sch 1(A35);
reconsider x = Fk as Element of the carrier of L * by FINSEQ_1:def 11;
take x ; :: thesis:
take a1' ; :: thesis:
take b1' ; :: thesis:
take Fk ; :: thesis:
take pa1' ; :: thesis:
take qb1' ; :: thesis:
thus ( pa1' = p . a1' & qb1' = q . b1' & Fk = x ) ; :: thesis:
thus (decomp b1) /. k = <*a1',b1'*> by A34; :: thesis:
thus len Fk = len (decomp b2) by A37, FINSEQ_1:def 3; :: thesis:
let m be Nat; :: thesis:
assume m in dom Fk ; :: thesis:
hence ex a1'', b1'' being bag of o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) by A37, A38; :: thesis:

end;

consider F being FinSequence of the carrier of L * such that
A39: dom F = Seg (len r) and
A40: for k being Element of NAT st k in Seg (len r) holds
S₂[k,F /. k] from POLYNOM2:sch 1(A33);
take s = FlattenSeq F; :: thesis:
A41: len (Sum F) = len F by MATRLIN:def 8;
reconsider rFFb2 = rFFb2 as FinSequence of the carrier of L by A26, FINSEQ_1:def 4;
A42: f . x = Compress (p *' q) by A2;
A43: dom rFFb2 = dom F by A39, A24, FINSEQ_1:def 3
.= dom (Sum F) by A41, FINSEQ_3:31 ;
for k being Nat st k in dom rFFb2 holds
rFFb2 . k = (Sum F) . k

proof

let k be Nat; :: thesis:
assume A44: k in dom rFFb2 ; :: thesis:
consider c1, d1 being bag of o1 such that
A45: (decomp b1) /. k = <*c1,d1*> and
A46: r /. k = (p . c1) * (q . d1) by A22, A24, A44;
k in Seg (len r) by A24, A44, FINSEQ_1:def 3;
then consider a1', b1' being bag of o1, Fk being FinSequence of the carrier of L, pa1', qb1' being Polynomial of o2,L such that
A47: ( pa1' = p . a1' & qb1' = q . b1' ) and
A48: Fk = F /. k and
A49: (decomp b1) /. k = <*a1',b1'*> and
A50: len Fk = len (decomp b2) and
A51: for ki being Nat st ki in dom Fk holds
ex a1'', b1'' being bag of o2 st
( (decomp b2) /. ki = <*a1'',b1''*> & Fk /. ki = (pa1' . a1'') * (qb1' . b1'') ) by A40;
A52: ( c1 = a1' & d1 = b1' ) by A45, A49, FINSEQ_1:98;
consider s1 being FinSequence of the carrier of L such that
A53: (pa1' *' qb1') . b2 = Sum s1 and
A54: len s1 = len (decomp b2) and
A55: 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 = (pa1' . x1) * (qb1' . y2) ) by POLYNOM1:def 26;
A56: dom s1 = Seg (len s1) by FINSEQ_1:def 3;

now

let ki be Nat; :: thesis:
assume A57: ki in dom s1 ; :: thesis:
then A58: s1 /. ki = s1 . ki by PARTFUN1:def 8;
A59: ki in dom Fk by A50, A54, A56, A57, FINSEQ_1:def 3;
then consider a1'', b1'' being bag of o2 such that
A60: (decomp b2) /. ki = <*a1'',b1''*> and
A61: Fk /. ki = (pa1' . a1'') * (qb1' . b1'') by A51;
consider x1, y2 being bag of o2 such that
A62: (decomp b2) /. ki = <*x1,y2*> and
A63: s1 /. ki = (pa1' . x1) * (qb1' . y2) by A55, A57;
( x1 = a1'' & y2 = b1'' ) by A62, A60, FINSEQ_1:98;
hence s1 . ki = Fk . ki by A63, A59, A61, A58, PARTFUN1:def 8; :: thesis:

end;

then A64: s1 = Fk by A50, A54, FINSEQ_2:10;
A65: rFF . k = r /. k by A24, A44, PARTFUN1:def 8
.= pa1' *' qb1' by A46, A47, A52, POLYNOM1:def 27 ;
thus rFFb2 . k = (rFF . k) . b2 by A24, A25, A44
.= (Sum F) /. k by A43, A44, A48, A65, A53, A64, MATRLIN:def 8
.= (Sum F) . k by A43, A44, PARTFUN1:def 8 ; :: thesis:

end;

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

proof

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

end;

consider ff being Function of NAT ,the carrier of L such that
A72: for j being Element of NAT holds S₃[j,ff . j] from FUNCT_2:sch 3(A70);
defpred S₄[ set , set ] means ex a1', b1' being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = $2 & (decomp b1) /. $1 = <*a1',b1'*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = <*(a1' +^ a1''),(b1' +^ b1'')*> ) ) );
A73: for i being Element of 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 Element of NAT ; :: thesis:
assume k in Seg (len r) ; :: thesis:
then k in dom (decomp b1) by A21, FINSEQ_1:def 3;
then consider a1', b1' being bag of o1 such that
A74: (decomp b1) /. k = <*a1',b1'*> and
b1 = a1' + b1' by PRE_POLY:68;
reconsider a1' = a1', b1' = b1' as Element of Bags o1 by PRE_POLY:def 12;
defpred S₅[ set , set ] means ex a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. $1 = <*a1'',b1''*> & $2 = <*(a1' +^ a1''),(b1' +^ b1'')*> );
A75: for k being Element of 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 Element of NAT ; :: thesis:
assume k in Seg (len (decomp b2)) ; :: thesis:
then k in dom (decomp b2) by FINSEQ_1:def 3;
then consider a1'', b1'' being bag of o2 such that
A76: (decomp b2) /. k = <*a1'',b1''*> and
b2 = a1'' + b1'' by PRE_POLY:68;
reconsider a1'' = a1'', b1'' = b1'' as Element of Bags o2 by PRE_POLY:def 12;
reconsider x = <*(a1' +^ a1''),(b1' +^ b1'')*> as Element of 2 -tuples_on (Bags (o1 +^ o2)) ;
take x ; :: thesis:
take a1'' ; :: thesis:
take b1'' ; :: thesis:
thus ( (decomp b2) /. k = <*a1'',b1''*> & x = <*(a1' +^ a1''),(b1' +^ b1'')*> ) 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 Element of NAT st k in Seg (len (decomp b2)) holds
S₅[k,Fk /. k] from POLYNOM2:sch 1(A75);
reconsider x = Fk as Element of (2 -tuples_on (Bags (o1 +^ o2))) * by FINSEQ_1:def 11;
take x ; :: thesis:
take a1' ; :: thesis:
take b1' ; :: thesis:
take Fk ; :: thesis:
thus Fk = x ; :: thesis:
thus (decomp b1) /. k = <*a1',b1'*> 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 a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = <*(a1' +^ a1''),(b1' +^ b1'')*> ) 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 Element of NAT st i in Seg (len r) holds
S₄[i,G /. i] from POLYNOM2:sch 1(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 a1', b1' being bag of o1 ex Fk being FinSequence of the carrier of L ex pa1', qb1' being Polynomial of o2,L st
( pa1' = p . a1' & qb1' = q . b1' & Fk = F /. j & (decomp b1) /. j = <*a1',b1'*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a1'', b1'' being bag of o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) ) ) & ex a2', b2' being Element of Bags o1 ex Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Gk = G /. j & (decomp b1) /. j = <*a2',b2'*> & len Gk = len (decomp b2) & ( for m being Nat st m in dom Gk holds
ex a2'', b2'' being Element of Bags o2 st
( (decomp b2) /. m = <*a2'',b2''*> & Gk /. m = <*(a2' +^ a2''),(b2' +^ b2'')*> ) ) ) ) by A39, A40, A80, A85;
card (F . j) = card (F /. j) by A85, PARTFUN1:def 8
.= card (G . j) by A39, A79, A82, A84, A87, PARTFUN1:def 8 ;
hence (Card F) . j = (Card G) . j by A39, 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 A19, A89, Th7;
then dom G = dom (decomp c1) by A21, A79, FINSEQ_1:def 3;
then A92: decomp c = FlattenSeq G by A19, A79, A81, A91, Th14;
A93: for j being Element of NAT
for v being Element of st j < len rFFb2 & v = rFFb2 . (j + 1) holds
ff . (j + 1) = (ff . j) + v

proof

let j be Element of NAT ; :: thesis:
let v be Element of ; :: thesis:
assume that
A94: j < len rFFb2 and
A95: v = rFFb2 . (j + 1) ; :: thesis:
reconsider w = r /. (j + 1), pp = gg . j, pp' = gg . (j + 1) as Polynomial of o2,L by POLYNOM1:def 27;
reconsider w1 = w, pp1 = pp, pp1' = pp' as Element of ;
reconsider w1 = w1, pp1 = pp1, pp1' = pp1' as Element of ;
A96: j < len r by A24, A94, FINSEQ_3:31;
then A97: j + 1 <= len r by NAT_1:13;
then A98: w = r . (j + 1) by FINSEQ_4:24, NAT_1:11;
then A99: pp1' = pp1 + w1 by A69, A96;
1 <= j + 1 by NAT_1:11;
then j + 1 in dom r by A97, FINSEQ_3:27;
then A100: w . b2 = v by A25, A95, A98;
j + 1 <= len r by A96, NAT_1:13;
hence ff . (j + 1) = pp' . b2 by A72
.= (pp + w) . b2 by A99, POLYNOM1:def 27
.= (pp . b2) + (w . b2) by POLYNOM1:def 21
.= (ff . j) + v by A72, A96, A100 ;
:: thesis:

end;

gg . 0 = 0_ o2,L by A68, POLYNOM1:def 27;
then A101: ff . 0 = (0_ o2,L) . b2 by A72, NAT_1:2
.= 0. L by POLYNOM1:81 ;
len rFFb2 = len r by A24, FINSEQ_3:31;
then Sr . b2 = ff . (len rFFb2) by A67, A72;
then A102: Sr . b2 = Sum rFFb2 by A101, A93, RLVECT_1:def 13;
( b1 = c1 & b2 = c2 ) by A19, A89, Th7;
hence fpq' . c = Sum s by A20, A88, A90, A66, A102, A42, POLYNOM1:34; :: thesis:
dom (Card G) = dom G by CARD_3:def 2;
then len (Card F) = len (Card G) by A39, A79, A82, FINSEQ_3:31;
then A103: Card F = Card G by A83, FINSEQ_2:10;
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 Element of 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:31;
then consider i', j' being Element of NAT such that
A111: i' in dom G and
A112: j' in dom (G . i') and
A113: k = (Sum (Card (G | (i' -' 1)))) + j' and
A114: (G . i') . j' = (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) | (i' -' 1))) + j' by A108, A113, POLYNOM3:16 ;
then A115: ( i = i' & j = j' ) 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 a1', b1' being bag of o1, Fk being FinSequence of the carrier of L, pa1', qb1' being Polynomial of o2,L such that
A120: pa1' = p . a1' and
A121: qb1' = q . b1' and
A122: Fk = F /. i and
A123: (decomp b1) /. i = <*a1',b1'*> and
len Fk = len (decomp b2) and
A124: for m being Nat st m in dom Fk holds
ex a1'', b1'' being bag of o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) by A39, A40, A106;
consider ga1', gb1' 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 = <*ga1',gb1'*> and
len Gk = len (decomp b2) and
A127: for m being Nat st m in dom Gk holds
ex ga1'', gb1'' being Element of Bags o2 st
( (decomp b2) /. m = <*ga1'',gb1''*> & Gk /. m = <*(ga1' +^ ga1''),(gb1' +^ gb1'')*> ) by A39, A80, A106;
A128: b1' = gb1' by A123, A126, FINSEQ_1:98;
A129: Gk = G . i by A39, A79, A106, A125, PARTFUN1:def 8;
then consider ga1'', gb1'' being Element of Bags o2 such that
A130: (decomp b2) /. j = <*ga1'',gb1''*> and
A131: Gk /. j = <*(ga1' +^ ga1''),(gb1' +^ gb1'')*> by A112, A115, A127;
A132: <*c1,c2*> = (G . i) . j by A110, A116, A114, A115, PARTFUN1:def 8
.= <*(ga1' +^ ga1''),(gb1' +^ gb1'')*> by A112, A115, A129, A131, PARTFUN1:def 8 ;
then c1 = ga1' +^ ga1'' by FINSEQ_1:98;
then A133: ( cb1 = ga1' & cb2 = ga1'' ) by A118, Th7;
A134: a1' = ga1' by A123, A126, FINSEQ_1:98;
j in dom Fk by A106, A107, A122, PARTFUN1:def 8;
then consider a1'', b1'' being bag of o2 such that
A135: (decomp b2) /. j = <*a1'',b1''*> and
A136: Fk /. j = (pa1' . a1'') * (qb1' . b1'') by A124;
a1'' = ga1'' by A130, A135, FINSEQ_1:98;
then A137: pa1' . a1'' = 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 = gb1' +^ gb1'' by A132, FINSEQ_1:98;
then A141: ( cb1 = gb1' & cb2 = gb1'' ) by A139, Th7;
A142: Fk = F . i by A106, A122, PARTFUN1:def 8;
b1'' = gb1'' by A130, A135, FINSEQ_1:98;
then A143: qb1' . b1'' = fq . c2 by A2, A121, A128, A138, A140, A141;
thus s /. k = s . k by A105, PARTFUN1:def 8
.= (fp . c1) * (fq . c2) by A107, A109, A142, A136, A137, A143, PARTFUN1:def 8 ; :: thesis:

end;

thus f . (x * y) = f . (p *' q) by POLYNOM1:def 27
.= fp *' fq by A18, POLYNOM1:def 26
.= (f . x) * (f . y) by POLYNOM1:def 27 ; :: thesis:

end;

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

proof

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

per cases ;

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

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

end;

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

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

now

per cases ;

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

Q1 = (1_ o1,(Polynom-Ring o2,L)) . b1 by A147, POLYNOM1:90
.= 1_ (Polynom-Ring o2,L) by A155, POLYNOM1:84
.= 1_ o2,L by POLYNOM1:90 ;
then Q1 . b2 = 0. L by A154, A155, POLYNOM1:84
.= 1P2 . b by A146, A153, POLYNOM1:84 ;
hence (Compress 1P1) . b = 1P2 . b by A149; :: thesis:

end;

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

Q1 = (1_ o1,(Polynom-Ring o2,L)) . b1 by A147, POLYNOM1:90
.= 0. (Polynom-Ring o2,L) by A156, POLYNOM1:84
.= 0_ o2,L by POLYNOM1:def 27 ;
then Q1 . b2 = 0. L by POLYNOM1:81
.= 1P2 . b by A146, A153, POLYNOM1:84 ;
hence (Compress 1P1) . b = 1P2 . b by A149; :: 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 A145, FUNCT_2:113 ;
hence A157: f is unity-preserving by GROUP_1:def 17; :: thesis:
thus f is one-to-one :: thesis:

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume x1 in dom f ; :: thesis:
then reconsider x1' = x1 as Element of by FUNCT_2:def 1;
assume x2 in dom f ; :: thesis:
then reconsider x2' = x2 as Element of by FUNCT_2:def 1;
reconsider x2'' = x2' as Polynomial of o1, Polynom-Ring o2,L by POLYNOM1:def 27;
reconsider x1'' = x1' as Polynomial of o1, Polynom-Ring o2,L by POLYNOM1:def 27;
A158: f . x2' = Compress x2'' by A2;
then reconsider w2 = f . x2' as Polynomial of (o1 +^ o2),L ;
A159: f . x1' = Compress x1'' by A2;
then reconsider w1 = f . x1' as Polynomial of (o1 +^ o2),L ;
assume A160: f . x1 = f . x2 ; :: thesis:

now

let b1 be Element of Bags o1; :: thesis:
reconsider x1''b1 = x1'' . b1, x2''b1 = x2'' . b1 as Polynomial of o2,L by POLYNOM1:def 27;

now

let b2 be Element of Bags o2; :: thesis:
set b = b1 +^ b2;
consider b1' being Element of Bags o1, b2' being Element of Bags o2, Q1 being Polynomial of o2,L such that
A161: Q1 = x1'' . b1' and
A162: b1 +^ b2 = b1' +^ b2' and
A163: w1 . (b1 +^ b2) = Q1 . b2' by A159, Def2;
A164: ( b1 = b1' & b2 = b2' ) by A162, Th7;
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1' being Polynomial of o2,L such that
A165: Q1' = x2'' . c1 and
A166: b1 +^ b2 = c1 +^ c2 and
A167: w2 . (b1 +^ b2) = Q1' . c2 by A158, Def2;
b1 = c1 by A166, Th7;
hence x1''b1 . b2 = x2''b1 . b2 by A160, A161, A163, A165, A166, A167, A164, Th7; :: thesis:

end;

hence x1'' . b1 = x2'' . b1 by FUNCT_2:113; :: thesis:

end;

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

end;

thus f is RingHomomorphism by A3, A144, A157; :: according to QUOFIELD:def 22 :: thesis:
thus rng f c= the carrier of (Polynom-Ring (o1 +^ o2),L) by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: 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 set ; :: 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 27;
defpred S₃[ Element of Bags o1, Element of ] 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 ) );
A168: 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
A169: 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 A169; :: thesis:
thus y = b1 ; :: thesis:

end;

consider kk being Function of Bags (o1 +^ o2), Bags o1 such that
A170: for b being Element of Bags (o1 +^ o2) holds S₂[b,kk . b] from FUNCT_2:sch 3(A168);
A171: for x being Element of Bags o1 ex y being Element of 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 ] means for b being Element of Bags (o1 +^ o2) st b = b1 +^ $1 holds
$2 = s . b;
A172: for p being Element of Bags o2 ex q being Element of st S₅[p,q]

proof

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

end;

consider t being Function of Bags o2,the carrier of L such that
A173: for b2 being Element of Bags o2 holds S₅[b2,t . b2] from FUNCT_2:sch 3(A172);
reconsider t = t as Function of Bags o2,L ;
A174: 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
A175: 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 A175; :: thesis:
thus y = b2 ; :: thesis:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A177: x in Support t ; :: thesis:
then reconsider b2 = x as Element of Bags o2 ;
set b = b1 +^ b2;
t . x <> 0. L by A177, POLYNOM1:def 9;
then s . (b1 +^ b2) <> 0. L by A173;
then A178: ( dom kk = Bags (o1 +^ o2) & b1 +^ b2 in Support s ) by FUNCT_2:def 1, POLYNOM1:def 9;
ex b1' being Element of Bags o1 ex b2' being Element of Bags o2 st
( b1 +^ b2 = b1' +^ b2' & kk . (b1 +^ b2) = b2' ) by A176;
then x = kk . (b1 +^ b2) by Th7;
hence x in kk .: (Support s) by A178, FUNCT_1:def 12; :: thesis:

end;

then t is Polynomial of o2,L by POLYNOM1:def 10;
then reconsider t'' = t as Element of by POLYNOM1:def 27;
reconsider t' = t as Function ;
take t'' ; :: thesis:
take t' ; :: thesis:
thus t'' = t' ; :: thesis:
let b2 be Element of Bags o2; :: thesis:
let b be Element of Bags (o1 +^ o2); :: thesis:
assume b = x +^ b2 ; :: thesis:
hence t' . b2 = s . b by A173; :: thesis:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A181: x in Support g ; :: thesis:
then reconsider b1 = x as Element of Bags o1 ;
consider h being Function such that
A182: h = g . b1 and
A183: 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 A179;
reconsider h = h as Polynomial of o2,L by A182, POLYNOM1:def 27;
g . b1 <> 0. (Polynom-Ring o2,L) by A181, POLYNOM1:def 9;
then g . b1 <> 0_ o2,L by POLYNOM1:def 27;
then consider b2 being Element of Bags o2 such that
A184: b2 in Support h by A182, POLYNOM2:19, SUBSET_1:10;
set b = b1 +^ b2;
h . b2 <> 0. L by A184, POLYNOM1:def 9;
then s . (b1 +^ b2) <> 0. L by A183;
then A185: ( dom kk = Bags (o1 +^ o2) & b1 +^ b2 in Support s ) by FUNCT_2:def 1, POLYNOM1:def 9;
ex b1' being Element of Bags o1 ex b2' being Element of Bags o2 st
( b1 +^ b2 = b1' +^ b2' & kk . (b1 +^ b2) = b1' ) by A170;
then x = kk . (b1 +^ b2) by Th7;
hence x in kk .: (Support s) by A185, FUNCT_1:def 12; :: thesis:

end;

then g is Polynomial of o1, Polynom-Ring o2,L by POLYNOM1:def 10;
then reconsider g = g as Element of by POLYNOM1:def 27;
reconsider g' = g as Polynomial of o1, Polynom-Ring o2,L by A180, POLYNOM1:def 10;

now

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
A186: ( Q1 = g' . b1 & b = b1 +^ b2 & (Compress g') . b = Q1 . b2 ) by Def2;
ex h being Function st
( h = g' . 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 A179;
hence s . b = (Compress g') . b by A186; :: thesis:

end;

then A187: y = Compress g' by FUNCT_2:113
.= 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 A187, FUNCT_1:12; :: thesis:

end;