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

proof

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 27;
reconsider u = Compress Q as Element of (Polynom-Ring (o1 +^ o2),L) 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 (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 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 (Polynom-Ring o1,(Polynom-Ring o2,L)); :: according to GRCAT_1:def 13 :: thesis:
reconsider x' = x, y' = y as Element of (Polynom-Ring o1,(Polynom-Ring o2,L)) ;
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 (Polynom-Ring (o1 +^ o2),L) ;
reconsider fp = fp, fq = fq, fpq = fpq as Polynomial of (o1 +^ o2),L by POLYNOM1:def 27;
for x being bag of holds fpq . x = (fp . x) + (fq . x)

proof

let b be bag of ; :: thesis:
reconsider b' = b as Element of Bags (o1 +^ o2) by POLYNOM1:def 14;
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;
reconsider b1 = b1 as bag of ;
A13: ( b1 = b1' & b1' = b1'' & b1 = b1'' & b2 = b2' & b2' = b2'' & b2 = b2'' ) by A5, A8, A11, Th7;
(p + q) . b1 = (p . b1) + (q . b1) by POLYNOM1:def 21;
then Q1'' = Q1 + Q1' by A4, A7, A10, A13, POLYNOM1:def 27;
then A14: Q1'' . b2 = (Q1 . b2) + (Q1' . b2) by POLYNOM1:def 21;
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, A13, A14
.= (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;

thus A15: f is multiplicative :: thesis:

proof

now

let x, y be Element of (Polynom-Ring o1,(Polynom-Ring o2,L)); :: thesis:
reconsider x' = x, y' = y as Element of (Polynom-Ring o1,(Polynom-Ring o2,L)) ;
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 (Polynom-Ring (o1 +^ o2),L) ;
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;
A16: for b being bag of 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 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

proof

let c be bag of ; :: thesis:
reconsider b = c as Element of Bags (o1 +^ o2) by POLYNOM1:def 14;
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A17: b = b1 +^ b2 by Th6;
reconsider b1 = b1 as bag of ;
consider r being FinSequence of the carrier of (Polynom-Ring o2,L) such that
A18: (p *' q) . b1 = Sum r and
A19: len r = len (decomp b1) and
A20: for k being Element of NAT st k in dom r holds
ex a1', b1' being bag of st
( (decomp b1) /. k = <*a1',b1'*> & r /. k = (p . a1') * (q . b1') ) by POLYNOM1:def 26;
defpred S₂[ set , set ] means ex a1', b1' being bag of 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 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) ) );
A21: 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 A19, FINSEQ_1:def 3;
then consider a1', b1' being bag of such that
A22: ( (decomp b1) /. k = <*a1',b1'*> & b1 = a1' + b1' ) by POLYNOM1:72;
reconsider pa1'' = p . a1', qb1'' = q . b1' as Element of (Polynom-Ring o2,L) ;
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 st
( (decomp b2) /. $1 = <*a1'',b1''*> & $2 = (pa1' . a1'') * (qb1' . b1'') );
A23: for k being Element of NAT st k in Seg (len (decomp b2)) holds
ex x being Element of L 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 such that
A24: ( (decomp b2) /. k = <*a1'',b1''*> & b2 = a1'' + b1'' ) by POLYNOM1:72;
reconsider x = (pa1' . a1'') * (qb1' . b1'') as Element of L ;
take x ; :: thesis:
take a1'' ; :: thesis:
take b1'' ; :: thesis:
thus ( (decomp b2) /. k = <*a1'',b1''*> & x = (pa1' . a1'') * (qb1' . b1'') ) by A24; :: thesis:

end;

consider Fk being FinSequence of the carrier of L such that
A25: dom Fk = Seg (len (decomp b2)) and
A26: for k being Element of NAT st k in Seg (len (decomp b2)) holds
S₃[k,Fk /. k] from POLYNOM2:sch 1(A23);
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 A22; :: thesis:
thus len Fk = len (decomp b2) by A25, FINSEQ_1:def 3; :: thesis:
let m be Nat; :: thesis:
assume m in dom Fk ; :: thesis:
hence ex a1'', b1'' being bag of st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) by A25, A26; :: thesis:

end;

consider F being FinSequence of the carrier of L * such that
A27: dom F = Seg (len r) and
A28: for k being Element of NAT st k in Seg (len r) holds
S₂[k,F /. k] from POLYNOM2:sch 1(A21);
take s = FlattenSeq F; :: thesis:
reconsider x = p *' q as Element of (Polynom-Ring o1,(Polynom-Ring o2,L)) by POLYNOM1:def 27;
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A29: Q1 = (p *' q) . c1 and
A30: b = c1 +^ c2 and
A31: (Compress (p *' q)) . b = Q1 . c2 by Def2;
A32: ( b1 = c1 & b2 = c2 ) by A17, A30, Th7;
reconsider Sr = Sum r as Polynomial of o2,L by POLYNOM1:def 27;
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 A33: 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 A33, 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
A34: dom rFFb2 = dom r and
A35: for i being set st i in dom r holds
rFFb2 . i = H₁(i) from FUNCT_1:sch 3();
consider i being Nat such that
A36: dom r = Seg i by FINSEQ_1:def 2;
reconsider rFFb2 = rFFb2 as FinSequence by A34, A36, FINSEQ_1:def 2;
rng rFFb2 c= the carrier of L

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in rng rFFb2 ; :: thesis:
then consider x being set such that
A37: x in dom rFFb2 and
A38: u = rFFb2 . x by FUNCT_1:def 5;
A39: rFFb2 . x = (rFF . x) . b2 by A34, A35, A37;
A40: rFF . x in rng rFF by A34, A37, FUNCT_1:12;
rng rFF c= the carrier of (Polynom-Ring o2,L) by FINSEQ_1:def 4;
then A41: rFF . x is Function of (Bags o2),the carrier of L by A40, POLYNOM1:def 27;
then A42: rng (rFF . x) c= the carrier of L by RELAT_1:def 19;
dom (rFF . x) = Bags o2 by A41, FUNCT_2:def 1;
then (rFF . x) . b2 in rng (rFF . x) by FUNCT_1:12;
hence u in the carrier of L by A38, A39, A42; :: thesis:

end;

then reconsider rFFb2 = rFFb2 as FinSequence of the carrier of L by FINSEQ_1:def 4;
A43: len (Sum F) = len F by MATRLIN:def 8;
A44: dom rFFb2 = dom F by A27, A34, FINSEQ_1:def 3
.= dom (Sum F) by A43, 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 A45: k in dom rFFb2 ; :: thesis:
consider c1, d1 being bag of such that
A46: (decomp b1) /. k = <*c1,d1*> and
A47: r /. k = (p . c1) * (q . d1) by A20, A34, A45;
k in Seg (len r) by A34, A45, FINSEQ_1:def 3;
then consider a1', b1' being bag of , Fk being FinSequence of the carrier of L, pa1', qb1' being Polynomial of o2,L such that
A48: ( pa1' = p . a1' & qb1' = q . b1' ) and
A49: Fk = F /. k and
A50: (decomp b1) /. k = <*a1',b1'*> and
A51: len Fk = len (decomp b2) and
A52: for ki being Nat st ki in dom Fk holds
ex a1'', b1'' being bag of st
( (decomp b2) /. ki = <*a1'',b1''*> & Fk /. ki = (pa1' . a1'') * (qb1' . b1'') ) by A28;
A53: ( c1 = a1' & d1 = b1' ) by A46, A50, GROUP_7:2;
A54: rFF . k = r /. k by A34, A45, PARTFUN1:def 8
.= pa1' *' qb1' by A47, A48, A53, POLYNOM1:def 27 ;
consider s1 being FinSequence of the carrier of L such that
A55: (pa1' *' qb1') . b2 = Sum s1 and
A56: len s1 = len (decomp b2) and
A57: for ki being Element of NAT st ki in dom s1 holds
ex x1, y2 being bag of st
( (decomp b2) /. ki = <*x1,y2*> & s1 /. ki = (pa1' . x1) * (qb1' . y2) ) by POLYNOM1:def 26;
X: dom s1 = Seg (len s1) by FINSEQ_1:def 3;

now

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

end;

then A66: s1 = Fk by A51, A56, FINSEQ_2:10;
thus rFFb2 . k = (rFF . k) . b2 by A34, A35, A45
.= (Sum F) /. k by A44, A45, A49, A54, A55, A66, MATRLIN:def 8
.= (Sum F) . k by A44, A45, PARTFUN1:def 8 ; :: thesis:

end;

then A67: rFFb2 = Sum F by A44, FINSEQ_1:17;
consider gg being Function of NAT ,the carrier of (Polynom-Ring o2,L) such that
A68: Sum r = gg . (len r) and
A69: gg . 0 = 0. (Polynom-Ring o2,L) and
A70: for j being Element of 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 13;
defpred S₃[ Nat, set ] means for pp being Polynomial of o2,L st $1 <= len r & pp = gg . $1 holds
$2 = pp . b2;
A71: 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 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 ( x <= len r & pp = gg . x ) ; :: thesis:
hence y = pp . b2 ; :: 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(A71);
len rFFb2 = len r by A34, FINSEQ_3:31;
then A73: Sr . b2 = ff . (len rFFb2) by A68, A72;
gg . 0 = 0_ o2,L by A69, POLYNOM1:def 27;
then A74: ff . 0 = (0_ o2,L) . b2 by A72, NAT_1:2
.= 0. L by POLYNOM1:81 ;
for j being Element of 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 Element of NAT ; :: thesis:
let v be Element of L; :: thesis:
assume A75: ( j < len rFFb2 & v = rFFb2 . (j + 1) ) ; :: thesis:
then A76: j < len r by A34, FINSEQ_3:31;
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 (Polynom-Ring o2,L) ;
reconsider w1 = w1, pp1 = pp1, pp1' = pp1' as Element of (Polynom-Ring o2,L) ;
A77: 1 <= j + 1 by NAT_1:11;
A78: j + 1 <= len r by A76, NAT_1:13;
then A79: w = r . (j + 1) by FINSEQ_4:24, NAT_1:11;
j + 1 in dom r by A77, A78, FINSEQ_3:27;
then A80: w . b2 = v by A35, A75, A79;
A81: j + 1 <= len r by A76, NAT_1:13;
A82: pp1' = pp1 + w1 by A70, A76, A79;
thus ff . (j + 1) = pp' . b2 by A72, A81
.= (pp + w) . b2 by A82, POLYNOM1:def 27
.= (pp . b2) + (w . b2) by POLYNOM1:def 21
.= (ff . j) + v by A72, A76, A80 ; :: thesis:

end;

then A83: Sr . b2 = Sum rFFb2 by A73, A74, RLVECT_1:def 13;
f . x = Compress (p *' q) by A2;
hence fpq' . c = Sum s by A18, A29, A31, A32, A67, A83, POLYNOM1:34; :: thesis:
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'')*> ) ) );
A84: 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 A19, FINSEQ_1:def 3;
then consider a1', b1' being bag of such that
A85: ( (decomp b1) /. k = <*a1',b1'*> & b1 = a1' + b1' ) by POLYNOM1:72;
reconsider a1' = a1', b1' = b1' as Element of Bags o1 by POLYNOM1:def 14;
defpred S₅[ set , set ] means ex a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. $1 = <*a1'',b1''*> & $2 = <*(a1' +^ a1''),(b1' +^ b1'')*> );
A86: 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 such that
A87: ( (decomp b2) /. k = <*a1'',b1''*> & b2 = a1'' + b1'' ) by POLYNOM1:72;
reconsider a1'' = a1'', b1'' = b1'' as Element of Bags o2 by POLYNOM1:def 14;
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 A87; :: thesis:

end;

consider Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
A88: dom Fk = Seg (len (decomp b2)) and
A89: for k being Element of NAT st k in Seg (len (decomp b2)) holds
S₅[k,Fk /. k] from POLYNOM2:sch 1(A86);
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 A85; :: thesis:
thus len Fk = len (decomp b2) by A88, 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 A88, A89; :: thesis:

end;

consider G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * such that
A90: dom G = Seg (len r) and
A91: for i being Element of NAT st i in Seg (len r) holds
S₄[i,G /. i] from POLYNOM2:sch 1(A84);
A92: for i being Nat st i in Seg (len r) holds
S₄[i,G /. i] by A91;
A93: dom (Card G) = dom G by CARD_3:def 2;
A94: dom (Card F) = dom F by CARD_3:def 2;
then A95: len (Card F) = len (Card G) by A27, A90, A93, FINSEQ_3:31;
for j being Nat st j in dom (Card F) holds
(Card F) . j = (Card G) . j

proof

let j be Nat; :: thesis:
assume A96: j in dom (Card F) ; :: thesis:
then A97: j in dom (Card F) ;
A98: j in dom (Card G) by A27, A90, A93, A94, A96;
A99: j in dom F by A97, CARD_3:def 2;
A100: j in dom G by A27, A90, A94, A96;
A101: (Card F) . j = card (F . j) by A99, CARD_3:def 2;
consider a1', b1' being bag of , Fk being FinSequence of the carrier of L, pa1', qb1' being Polynomial of o2,L such that
( pa1' = p . a1' & qb1' = q . b1' ) and
A102: Fk = F /. j and
(decomp b1) /. j = <*a1',b1'*> and
A103: len Fk = len (decomp b2) and
for m being Nat st m in dom Fk holds
ex a1'', b1'' being bag of st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) by A27, A28, A99;
consider a2', b2' being Element of Bags o1, Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
A104: Gk = G /. j and
(decomp b1) /. j = <*a2',b2'*> and
A105: len Gk = len (decomp b2) and
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 A27, A91, A99;
card (F . j) = card (F /. j) by A99, PARTFUN1:def 8
.= card (G . j) by A93, A98, A102, A103, A104, A105, PARTFUN1:def 8 ;
hence (Card F) . j = (Card G) . j by A100, A101, CARD_3:def 2; :: thesis:

end;

then A106: Card F = Card G by A95, FINSEQ_2:10;
A107: ( c1 = b1 & c2 = b2 ) by A17, A30, Th7;
then dom G = dom (decomp c1) by A19, A90, FINSEQ_1:def 3;
then A108: decomp c = FlattenSeq G by A30, A90, A92, A107, Th14;
hence A109: len s = len (decomp c) by A106, POLYNOM1:31; :: thesis:
let k be Element of NAT ; :: thesis:
assume A110: k in dom s ; :: thesis:
then A111: k in dom (decomp c) by A109, FINSEQ_3:31;
then consider c1, c2 being bag of such that
A112: (decomp c) /. k = <*c1,c2*> and
c = c1 + c2 by POLYNOM1:72;
take c1 ; :: thesis:
take c2 ; :: thesis:
thus (decomp c) /. k = <*c1,c2*> by A112; :: thesis:
consider i, j being Element of NAT such that
A113: ( i in dom F & j in dom (F . i) ) and
A114: k = (Sum (Card (F | (i -' 1)))) + j and
A115: (F . i) . j = (FlattenSeq F) . k by A110, POLYNOM1:32;
consider i', j' being Element of NAT such that
A116: ( i' in dom G & j' in dom (G . i') ) and
A117: k = (Sum (Card (G | (i' -' 1)))) + j' and
A118: (G . i') . j' = (decomp c) . k by A108, A111, POLYNOM1:32;
(Sum ((Card F) | (i -' 1))) + j = (Sum (Card (F | (i -' 1)))) + j by POLYNOM3:16
.= (Sum ((Card G) | (i' -' 1))) + j' by A114, A117, POLYNOM3:16 ;
then A119: ( i = i' & j = j' ) by A106, A113, A116, POLYNOM3:22;
consider a1', b1' being bag of , 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 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = (pa1' . a1'') * (qb1' . b1'') ) by A27, A28, A113;
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 A27, A91, A113;
A128: Gk = G . i by A27, A90, A113, A125, PARTFUN1:def 8;
then consider ga1'', gb1'' being Element of Bags o2 such that
A129: (decomp b2) /. j = <*ga1'',gb1''*> and
A130: Gk /. j = <*(ga1' +^ ga1''),(gb1' +^ gb1'')*> by A116, A119, A127;
A131: Fk = F . i by A113, A122, PARTFUN1:def 8;
j in dom Fk by A113, A122, PARTFUN1:def 8;
then consider a1'', b1'' being bag of such that
A132: (decomp b2) /. j = <*a1'',b1''*> and
A133: Fk /. j = (pa1' . a1'') * (qb1' . b1'') by A124;
<*c1,c2*> = (G . i) . j by A111, A112, A118, A119, PARTFUN1:def 8
.= <*(ga1' +^ ga1''),(gb1' +^ gb1'')*> by A116, A119, A128, A130, PARTFUN1:def 8 ;
then A134: ( c1 = ga1' +^ ga1'' & c2 = gb1' +^ gb1'' ) by GROUP_7:2;
reconsider cc1 = c1, cc2 = c2 as Element of Bags (o1 +^ o2) by POLYNOM1:def 14;
consider cb1 being Element of Bags o1, cb2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A135: Q1 = p . cb1 and
A136: cc1 = cb1 +^ cb2 and
A137: (Compress p) . cc1 = Q1 . cb2 by Def2;
A138: ( cb1 = ga1' & cb2 = ga1'' ) by A134, A136, Th7;
A139: ( a1'' = ga1'' & b1'' = gb1'' ) by A129, A132, GROUP_7:2;
A140: ( a1' = ga1' & b1' = gb1' ) by A123, A126, GROUP_7:2;
then A141: pa1' . a1'' = fp . c1 by A2, A120, A135, A137, A138, A139;
consider cb1 being Element of Bags o1, cb2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A142: Q1 = q . cb1 and
A143: cc2 = cb1 +^ cb2 and
A144: (Compress q) . cc2 = Q1 . cb2 by Def2;
( cb1 = gb1' & cb2 = gb1'' ) by A134, A143, Th7;
then A145: qb1' . b1'' = fq . c2 by A2, A121, A139, A140, A142, A144;
thus s /. k = s . k by A110, PARTFUN1:def 8
.= (fp . c1) * (fq . c2) by A113, A115, A131, A133, A141, A145, PARTFUN1:def 8 ; :: thesis:

end;

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

end;

hence f is multiplicative by GROUP_6:def 7; :: thesis:

end;

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;
A146: for b being Element of Bags (o1 +^ o2) holds (Compress 1P1) . b = 1P2 . b

proof

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
A147: Q1 = 1P1 . b1 and
A148: b = b1 +^ b2 and
A149: (Compress 1P1) . b = Q1 . b2 by Def2;
A150: 1P2 . b = (1_ (o1 +^ o2),L) . b by POLYNOM1:90;

per cases ;

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

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

end;

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

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

now

per cases ;

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

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

end;

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

Q1 = (1_ o1,(Polynom-Ring o2,L)) . b1 by A147, POLYNOM1:90
.= 0. (Polynom-Ring o2,L) by A157, POLYNOM1:84
.= 0_ o2,L by POLYNOM1:def 27 ;
then Q1 . b2 = 0. L by POLYNOM1:81
.= 1P2 . b by A150, A154, 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 A146, FUNCT_2:113 ;
hence A158: 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 A159: x1 in dom f ; :: thesis:
assume A160: x2 in dom f ; :: thesis:
assume A161: f . x1 = f . x2 ; :: thesis:
reconsider x1' = x1 as Element of (Polynom-Ring o1,(Polynom-Ring o2,L)) by A159, FUNCT_2:def 1;
reconsider x1'' = x1' as Polynomial of o1,(Polynom-Ring o2,L) by POLYNOM1:def 27;
reconsider x2' = x2 as Element of (Polynom-Ring o1,(Polynom-Ring o2,L)) by A160, FUNCT_2:def 1;
reconsider x2'' = x2' as Polynomial of o1,(Polynom-Ring o2,L) by POLYNOM1:def 27;
A162: f . x2' = Compress x2'' by A2;
A163: f . x1' = Compress x1'' by A2;
then reconsider w1 = f . x1' as Polynomial of (o1 +^ o2),L ;
reconsider w2 = f . x2' as Polynomial of (o1 +^ o2),L by A162;

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
A164: Q1 = x1'' . b1' and
A165: b1 +^ b2 = b1' +^ b2' and
A166: w1 . (b1 +^ b2) = Q1 . b2' by A163, Def2;
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1' being Polynomial of o2,L such that
A167: Q1' = x2'' . c1 and
A168: b1 +^ b2 = c1 +^ c2 and
A169: w2 . (b1 +^ b2) = Q1' . c2 by A162, Def2;
( b1 = b1' & b1 = c1 & b2 = b2' & b2 = c2 & b1' = c1 & b2' = c2 ) by A165, A168, Th7;
hence x1''b1 . b2 = x2''b1 . b2 by A161, A164, A166, A167, A169; :: 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, A15, A158; :: 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

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 (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 ) );
A170: for x being Element of Bags o1 ex y being Element of (Polynom-Ring o2,L) st S₂[x,y]

proof

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

end;

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

proof

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

end;

then Support t is finite ;
then t is Polynomial of o2,L by POLYNOM1:def 10;
then reconsider t'' = t as Element of (Polynom-Ring o2,L) 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 A172; :: thesis:

end;

consider g being Function of (Bags o1),the carrier of (Polynom-Ring o2,L) such that
A182: for x being Element of Bags o1 holds S₂[x,g . x] from FUNCT_2:sch 3(A170);
reconsider g = g as Function of (Bags o1),(Polynom-Ring o2,L) ;
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 );
A183: 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
A184: 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 A184; :: thesis:
thus y = b1 ; :: thesis:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A186: x in Support g ; :: thesis:
then reconsider b1 = x as Element of Bags o1 ;
consider h being Function such that
A187: h = g . b1 and
A188: 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 A182;
g . b1 <> 0. (Polynom-Ring o2,L) by A186, POLYNOM1:def 9;
then A189: g . b1 <> 0_ o2,L by POLYNOM1:def 27;
reconsider h = h as Polynomial of o2,L by A187, POLYNOM1:def 27;
Support h <> {} by A187, A189, POLYNOM2:19;
then consider b2 being Element of Bags o2 such that
A190: b2 in Support h by SUBSET_1:10;
set b = b1 +^ b2;
A191: dom kk = Bags (o1 +^ o2) by FUNCT_2:def 1;
h . b2 <> 0. L by A190, POLYNOM1:def 9;
then s . (b1 +^ b2) <> 0. L by A188;
then A192: b1 +^ b2 in Support s by POLYNOM1:def 9;
consider b1' being Element of Bags o1, b2' being Element of Bags o2 such that
A193: b1 +^ b2 = b1' +^ b2' and
A194: kk . (b1 +^ b2) = b1' by A185;
x = kk . (b1 +^ b2) by A193, A194, Th7;
hence x in kk .: (Support s) by A191, A192, FUNCT_1:def 12; :: thesis:

end;

then A195: Support g is finite ;
then g is Polynomial of o1,(Polynom-Ring o2,L) by POLYNOM1:def 10;
then reconsider g = g as Element of (Polynom-Ring o1,(Polynom-Ring o2,L)) by POLYNOM1:def 27;
reconsider g' = g as Polynomial of o1,(Polynom-Ring o2,L) by A195, POLYNOM1:def 10;
A196: dom f = the carrier of (Polynom-Ring o1,(Polynom-Ring o2,L)) by FUNCT_2:def 1;

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
A197: Q1 = g' . b1 and
A198: b = b1 +^ b2 and
A199: (Compress g') . b = Q1 . b2 by Def2;
consider h being Function such that
A200: h = g' . b1 and
A201: 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 A182;
thus s . b = (Compress g') . b by A197, A198, A199, A200, A201; :: thesis:

end;

then y = Compress g' by FUNCT_2:113
.= f . g by A2 ;
hence y in rng f by A196, FUNCT_1:12; :: thesis:

end;