let o1, o2 be non empty Ordinal; :: thesis: for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic

let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic

set P2 = Polynom-Ring ((o1 +^ o2),L);

set P1 = Polynom-Ring (o1,(Polynom-Ring (o2,L)));

defpred S_{1}[ 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_{1}[x,u]

A2: for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) holds S_{1}[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: f is RingIsomorphism

thus f is additive :: according to RINGCAT1:def 1,MOD_4:def 8,MOD_4:def 12 :: thesis: ( f is multiplicative & f is unity-preserving & f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )

A144: for b being Element of Bags (o1 +^ o2) holds (Compress 1P1) . b = 1P2 . b

.= 1_ (Polynom-Ring ((o1 +^ o2),L)) by A144, FUNCT_2:63 ;

hence f is unity-preserving by GROUP_1:def 13; :: thesis: ( f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )

thus f is one-to-one :: thesis: f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L)))

thus the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= rng f :: thesis: verum

let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic

set P2 = Polynom-Ring ((o1 +^ o2),L);

set P1 = Polynom-Ring (o1,(Polynom-Ring (o2,L)));

defpred S

$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

proof

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
let x be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); :: thesis: ex u being Element of (Polynom-Ring ((o1 +^ o2),L)) st S_{1}[x,u]

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: S_{1}[x,u]

let P be Polynomial of o1,(Polynom-Ring (o2,L)); :: thesis: ( x = P implies u = Compress P )

assume x = P ; :: thesis: u = Compress P

hence u = Compress P ; :: thesis: verum

end;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: S

let P be Polynomial of o1,(Polynom-Ring (o2,L)); :: thesis: ( x = P implies u = Compress P )

assume x = P ; :: thesis: u = Compress P

hence u = Compress P ; :: thesis: verum

A2: for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) holds S

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: f is RingIsomorphism

thus f is additive :: according to RINGCAT1:def 1,MOD_4:def 8,MOD_4:def 12 :: thesis: ( f is multiplicative & f is unity-preserving & f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )

proof

let x, y be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)

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)

.= (f . x) + (f . y) by POLYNOM1:def 11 ;

:: thesis: verum

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

hence f . (x + y) =
fp + fq
by POLYNOM1:16
let b be bag of o1 +^ o2; :: thesis: fpq . b = (fp . b) + (fq . b)

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

end;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: verum

.= (f . x) + (f . y) by POLYNOM1:def 11 ;

:: thesis: verum

now :: thesis: for x, y being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) holds f . (x * y) = (f . x) * (f . y)

hence
f is multiplicative
by GROUP_6:def 6; :: thesis: ( f is unity-preserving & f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )let x, y be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); :: thesis: f . (x * y) = (f . x) * (f . y)

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

.= fp *' fq by A17, POLYNOM1:def 10

.= (f . x) * (f . y) by POLYNOM1:def 11 ; :: thesis: verum

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

thus f . (x * y) =
f . (p *' q)
by POLYNOM1:def 11
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: ex s being FinSequence of the carrier of L st

( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

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

deffunc H_{1}( 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_{1}(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_{2}[ 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_{2}[k,x]

A38: dom F = Seg (len r) and

A39: for k being Nat st k in Seg (len r) holds

S_{2}[k,F /. k]
from RECDEF_1:sch 17(A32);

take s = FlattenSeq F; :: thesis: ( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

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

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_{3}[ 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_{3}[x,y]

A71: for j being Element of NAT holds S_{3}[j,ff . j]
from FUNCT_2:sch 3(A69);

A72: for j being Nat holds S_{3}[j,ff . j]
_{4}[ 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_{4}[i,x]

A79: dom G = Seg (len r) and

A80: for i being Nat st i in Seg (len r) holds

S_{4}[i,G /. i]
from RECDEF_1:sch 17(A73);

A81: for i being Nat st i in Seg (len r) holds

S_{4}[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

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

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: ( len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

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: for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )

let k be Element of NAT ; :: thesis: ( k in dom s implies ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) )

assume A105: k in dom s ; :: thesis: ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )

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: ex b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*c1,b2*> & s /. k = (fp . c1) * (fq . b2) )

take c2 ; :: thesis: ( (decomp c) /. k = <*c1,c2*> & s /. k = (fp . c1) * (fq . c2) )

thus (decomp c) /. k = <*c1,c2*> by A116; :: thesis: s /. k = (fp . c1) * (fq . c2)

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

end;let c be bag of o1 +^ o2; :: thesis: ex s being FinSequence of the carrier of L st

( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

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

then reconsider rFF = r as Function-yielding Function by FUNCOP_1:def 6;
let x be object ; :: thesis: ( x in dom r implies r . x is Function )

assume x in dom r ; :: thesis: r . x is Function

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

end;assume x in dom r ; :: thesis: r . x is Function

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

deffunc H

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

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

defpred S
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng rFFb2 or u in the carrier of L )

A26: rng rFF c= the carrier of (Polynom-Ring (o2,L)) by FINSEQ_1:def 4;

assume u in rng rFFb2 ; :: thesis: u in the carrier of L

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

end;A26: rng rFF c= the carrier of (Polynom-Ring (o2,L)) by FINSEQ_1:def 4;

assume u in rng rFFb2 ; :: thesis: u in the carrier of L

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

( 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

proof

consider F being FinSequence of the carrier of L * such that
let k be Nat; :: thesis: ( k in Seg (len r) implies ex x being Element of the carrier of L * st S_{2}[k,x] )

assume k in Seg (len r) ; :: thesis: ex x being Element of the carrier of L * st S_{2}[k,x]

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_{3}[ 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_{3}[k,x]

A36: dom Fk = Seg (len (decomp b2)) and

A37: for k being Nat st k in Seg (len (decomp b2)) holds

S_{3}[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: S_{2}[k,x]

take a19 ; :: thesis: ex 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 = x & (decomp b1) /. k = <*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) ) ) )

take b19 ; :: thesis: 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 = x & (decomp b1) /. k = <*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) ) ) )

take Fk ; :: thesis: ex pa19, qb19 being Polynomial of o2,L st

( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*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) ) ) )

take pa19 ; :: thesis: ex qb19 being Polynomial of o2,L st

( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*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) ) ) )

take qb19 ; :: thesis: ( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*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) ) ) )

thus ( pa19 = p . a19 & qb19 = q . b19 & Fk = x ) ; :: thesis: ( (decomp b1) /. k = <*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) ) ) )

thus (decomp b1) /. k = <*a19,b19*> by A33; :: thesis: ( 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) ) ) )

thus len Fk = len (decomp b2) by A36, FINSEQ_1:def 3; :: thesis: 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) )

let m be Nat; :: thesis: ( m in dom Fk implies ex a199, b199 being bag of o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) )

assume m in dom Fk ; :: thesis: ex a199, b199 being bag of o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) )

hence ex a199, b199 being bag of o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) by A36, A37; :: thesis: verum

end;assume k in Seg (len r) ; :: thesis: ex x being Element of the carrier of L * st S

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

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

proof

consider Fk being FinSequence of the carrier of L such that
let k be Nat; :: thesis: ( k in Seg (len (decomp b2)) implies ex x being Element of L st S_{3}[k,x] )

assume k in Seg (len (decomp b2)) ; :: thesis: ex x being Element of L st S_{3}[k,x]

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: S_{3}[k,x]

take a199 ; :: thesis: ex b199 being bag of o2 st

( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) )

take b199 ; :: thesis: ( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) )

thus ( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) ) by A35; :: thesis: verum

end;assume k in Seg (len (decomp b2)) ; :: thesis: ex x being Element of L st S

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

take a199 ; :: thesis: ex b199 being bag of o2 st

( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) )

take b199 ; :: thesis: ( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) )

thus ( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) ) by A35; :: thesis: verum

A36: dom Fk = Seg (len (decomp b2)) and

A37: for k being Nat st k in Seg (len (decomp b2)) holds

S

reconsider x = Fk as Element of the carrier of L * by FINSEQ_1:def 11;

take x ; :: thesis: S

take a19 ; :: thesis: ex 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 = x & (decomp b1) /. k = <*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) ) ) )

take b19 ; :: thesis: 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 = x & (decomp b1) /. k = <*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) ) ) )

take Fk ; :: thesis: ex pa19, qb19 being Polynomial of o2,L st

( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*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) ) ) )

take pa19 ; :: thesis: ex qb19 being Polynomial of o2,L st

( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*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) ) ) )

take qb19 ; :: thesis: ( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*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) ) ) )

thus ( pa19 = p . a19 & qb19 = q . b19 & Fk = x ) ; :: thesis: ( (decomp b1) /. k = <*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) ) ) )

thus (decomp b1) /. k = <*a19,b19*> by A33; :: thesis: ( 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) ) ) )

thus len Fk = len (decomp b2) by A36, FINSEQ_1:def 3; :: thesis: 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) )

let m be Nat; :: thesis: ( m in dom Fk implies ex a199, b199 being bag of o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) )

assume m in dom Fk ; :: thesis: ex a199, b199 being bag of o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) )

hence ex a199, b199 being bag of o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) by A36, A37; :: thesis: verum

A38: dom F = Seg (len r) and

A39: for k being Nat st k in Seg (len r) holds

S

take s = FlattenSeq F; :: thesis: ( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

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

then A65:
rFFb2 = Sum F
by A42;
let k be Nat; :: thesis: ( k in dom rFFb2 implies rFFb2 . k = (Sum F) . k )

assume A43: k in dom rFFb2 ; :: thesis: rFFb2 . k = (Sum F) . k

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;

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

end;assume A43: k in dom rFFb2 ; :: thesis: rFFb2 . k = (Sum F) . k

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: for ki being Nat st ki in dom s1 holds

s1 . ki = Fk . ki

then A63:
s1 = Fk
by A49, A53, FINSEQ_2:9;s1 . ki = Fk . ki

let ki be Nat; :: thesis: ( ki in dom s1 implies s1 . ki = Fk . ki )

assume A56: ki in dom s1 ; :: thesis: s1 . ki = Fk . ki

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

end;assume A56: ki in dom s1 ; :: thesis: s1 . ki = Fk . ki

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

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

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

$2 = pp . b2;

A69: for x being Element of NAT ex y being Element of L st S

proof

consider ff being sequence of the carrier of L such that
let x be Element of NAT ; :: thesis: ex y being Element of L st S_{3}[x,y]

reconsider pp9 = gg . x as Polynomial of o2,L by POLYNOM1:def 11;

take y = pp9 . b2; :: thesis: S_{3}[x,y]

let pp be Polynomial of o2,L; :: thesis: ( x <= len r & pp = gg . x implies y = pp . b2 )

assume that

x <= len r and

A70: pp = gg . x ; :: thesis: y = pp . b2

thus y = pp . b2 by A70; :: thesis: verum

end;reconsider pp9 = gg . x as Polynomial of o2,L by POLYNOM1:def 11;

take y = pp9 . b2; :: thesis: S

let pp be Polynomial of o2,L; :: thesis: ( x <= len r & pp = gg . x implies y = pp . b2 )

assume that

x <= len r and

A70: pp = gg . x ; :: thesis: y = pp . b2

thus y = pp . b2 by A70; :: thesis: verum

A71: for j being Element of NAT holds S

A72: for j being Nat holds S

proof

defpred S
let n be Nat; :: thesis: S_{3}[n,ff . n]

n in NAT by ORDINAL1:def 12;

hence S_{3}[n,ff . n]
by A71; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence S

( 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

proof

consider G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * such that
let k be Nat; :: thesis: ( k in Seg (len r) implies ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S_{4}[k,x] )

assume k in Seg (len r) ; :: thesis: ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S_{4}[k,x]

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_{5}[ 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_{5}[k,x]

A77: dom Fk = Seg (len (decomp b2)) and

A78: for k being Nat st k in Seg (len (decomp b2)) holds

S_{5}[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: S_{4}[k,x]

take a19 ; :: thesis: ex b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st

( Fk = x & (decomp b1) /. k = <*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)*> ) ) )

take b19 ; :: thesis: ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st

( Fk = x & (decomp b1) /. k = <*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)*> ) ) )

take Fk ; :: thesis: ( Fk = x & (decomp b1) /. k = <*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)*> ) ) )

thus Fk = x ; :: thesis: ( (decomp b1) /. k = <*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)*> ) ) )

thus (decomp b1) /. k = <*a19,b19*> by A74; :: thesis: ( 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)*> ) ) )

thus len Fk = len (decomp b2) by A77, FINSEQ_1:def 3; :: thesis: 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)*> )

let m be Nat; :: thesis: ( m in dom Fk implies ex a199, b199 being Element of Bags o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) )

assume m in dom Fk ; :: thesis: ex a199, b199 being Element of Bags o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> )

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

end;assume k in Seg (len r) ; :: thesis: ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S

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

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

proof

consider Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
let k be Nat; :: thesis: ( k in Seg (len (decomp b2)) implies ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S_{5}[k,x] )

assume k in Seg (len (decomp b2)) ; :: thesis: ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S_{5}[k,x]

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: S_{5}[k,x]

take a199 ; :: thesis: ex b199 being Element of Bags o2 st

( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )

take b199 ; :: thesis: ( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )

thus ( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> ) by A76; :: thesis: verum

end;assume k in Seg (len (decomp b2)) ; :: thesis: ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S

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

take a199 ; :: thesis: ex b199 being Element of Bags o2 st

( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )

take b199 ; :: thesis: ( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )

thus ( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> ) by A76; :: thesis: verum

A77: dom Fk = Seg (len (decomp b2)) and

A78: for k being Nat st k in Seg (len (decomp b2)) holds

S

reconsider x = Fk as Element of (2 -tuples_on (Bags (o1 +^ o2))) * by FINSEQ_1:def 11;

take x ; :: thesis: S

take a19 ; :: thesis: ex b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st

( Fk = x & (decomp b1) /. k = <*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)*> ) ) )

take b19 ; :: thesis: ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st

( Fk = x & (decomp b1) /. k = <*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)*> ) ) )

take Fk ; :: thesis: ( Fk = x & (decomp b1) /. k = <*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)*> ) ) )

thus Fk = x ; :: thesis: ( (decomp b1) /. k = <*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)*> ) ) )

thus (decomp b1) /. k = <*a19,b19*> by A74; :: thesis: ( 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)*> ) ) )

thus len Fk = len (decomp b2) by A77, FINSEQ_1:def 3; :: thesis: 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)*> )

let m be Nat; :: thesis: ( m in dom Fk implies ex a199, b199 being Element of Bags o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) )

assume m in dom Fk ; :: thesis: ex a199, b199 being Element of Bags o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> )

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

A79: dom G = Seg (len r) and

A80: for i being Nat st i in Seg (len r) holds

S

A81: for i being Nat st i in Seg (len r) holds

S

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

consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
let j be Nat; :: thesis: ( j in dom (Card F) implies (Card F) . j = (Card G) . j )

assume A84: j in dom (Card F) ; :: thesis: (Card F) . j = (Card G) . j

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

end;assume A84: j in dom (Card F) ; :: thesis: (Card F) . j = (Card G) . j

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

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

gg . 0 = 0_ (o2,L)
by A67, POLYNOM1:def 11;
let j be Nat; :: thesis: for v being Element of L st j < len rFFb2 & v = rFFb2 . (j + 1) holds

ff . (j + 1) = (ff . j) + v

let v be Element of L; :: thesis: ( j < len rFFb2 & v = rFFb2 . (j + 1) implies ff . (j + 1) = (ff . j) + v )

assume that

A94: j < len rFFb2 and

A95: v = rFFb2 . (j + 1) ; :: thesis: ff . (j + 1) = (ff . j) + v

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

end;ff . (j + 1) = (ff . j) + v

let v be Element of L; :: thesis: ( j < len rFFb2 & v = rFFb2 . (j + 1) implies ff . (j + 1) = (ff . j) + v )

assume that

A94: j < len rFFb2 and

A95: v = rFFb2 . (j + 1) ; :: thesis: ff . (j + 1) = (ff . j) + v

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

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: ( len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )

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: for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )

let k be Element of NAT ; :: thesis: ( k in dom s implies ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) )

assume A105: k in dom s ; :: thesis: ex b1, b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )

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: ex b2 being bag of o1 +^ o2 st

( (decomp c) /. k = <*c1,b2*> & s /. k = (fp . c1) * (fq . b2) )

take c2 ; :: thesis: ( (decomp c) /. k = <*c1,c2*> & s /. k = (fp . c1) * (fq . c2) )

thus (decomp c) /. k = <*c1,c2*> by A116; :: thesis: s /. k = (fp . c1) * (fq . c2)

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

.= fp *' fq by A17, POLYNOM1:def 10

.= (f . x) * (f . y) by POLYNOM1:def 11 ; :: thesis: verum

A144: for b being Element of Bags (o1 +^ o2) holds (Compress 1P1) . b = 1P2 . b

proof

f . (1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L))))) =
Compress 1P1
by A2
let b be Element of Bags (o1 +^ o2); :: thesis: (Compress 1P1) . b = 1P2 . b

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;

end;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
( b = EmptyBag (o1 +^ o2) or b <> EmptyBag (o1 +^ o2) )
;

end;

suppose A149:
b = EmptyBag (o1 +^ o2)
; :: thesis: (Compress 1P1) . b = 1P2 . b

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

end;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: verum

suppose A152:
b <> EmptyBag (o1 +^ o2)
; :: thesis: (Compress 1P1) . b = 1P2 . b

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

end;now :: thesis: (Compress 1P1) . b = 1P2 . bend;

hence
(Compress 1P1) . b = 1P2 . b
; :: thesis: verumper cases
( b1 = EmptyBag o1 or b1 <> EmptyBag o1 )
;

end;

suppose A154:
b1 = EmptyBag o1
; :: thesis: (Compress 1P1) . b = 1P2 . b

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

end;.= 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: verum

suppose A155:
b1 <> EmptyBag o1
; :: thesis: (Compress 1P1) . b = 1P2 . b

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

end;.= 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: verum

.= 1_ (Polynom-Ring ((o1 +^ o2),L)) by A144, FUNCT_2:63 ;

hence f is unity-preserving by GROUP_1:def 13; :: thesis: ( f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )

thus f is one-to-one :: thesis: f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L)))

proof

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: the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= K734( the carrier of (Polynom-Ring ((o1 +^ o2),L)),f)
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume x1 in dom f ; :: thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

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: ( not f . x1 = f . x2 or x1 = x2 )

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: x1 = x2

end;assume x1 in dom f ; :: thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

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: ( not f . x1 = f . x2 or x1 = x2 )

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: x1 = x2

now :: thesis: for b1 being Element of Bags o1 holds x199 . b1 = x299 . b1

hence
x1 = x2
by FUNCT_2:63; :: thesis: verumlet b1 be Element of Bags o1; :: thesis: x199 . b1 = x299 . b1

reconsider x199b1 = x199 . b1, x299b1 = x299 . b1 as Polynomial of o2,L by POLYNOM1:def 11;

end;reconsider x199b1 = x199 . b1, x299b1 = x299 . b1 as Polynomial of o2,L by POLYNOM1:def 11;

now :: thesis: for b2 being Element of Bags o2 holds x199b1 . b2 = x299b1 . b2

hence
x199 . b1 = x299 . b1
by FUNCT_2:63; :: thesis: verumlet b2 be Element of Bags o2; :: thesis: x199b1 . b2 = x299b1 . b2

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

end;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: verum

thus the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= rng f :: thesis: verum

proof

defpred S_{2}[ 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: ( not y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) or y in rng f )

assume y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) ; :: thesis: y in rng f

then reconsider s = y as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;

defpred S_{3}[ 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_{2}[x,y]

A168: for b being Element of Bags (o1 +^ o2) holds S_{2}[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_{3}[x,y]

A177: for x being Element of Bags o1 holds S_{3}[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)

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;

.= 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: verum

end;( $1 = b1 +^ b2 & $2 = b1 );

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) or y in rng f )

assume y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) ; :: thesis: y in rng f

then reconsider s = y as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;

defpred S

( 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

proof

consider kk being Function of (Bags (o1 +^ o2)),(Bags o1) such that
let x be Element of Bags (o1 +^ o2); :: thesis: ex y being Element of Bags o1 st S_{2}[x,y]

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: S_{2}[x,y]

take b1 ; :: thesis: ex b2 being Element of Bags o2 st

( x = b1 +^ b2 & y = b1 )

take b2 ; :: thesis: ( x = b1 +^ b2 & y = b1 )

thus x = b1 +^ b2 by A167; :: thesis: y = b1

thus y = b1 ; :: thesis: verum

end;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: S

take b1 ; :: thesis: ex b2 being Element of Bags o2 st

( x = b1 +^ b2 & y = b1 )

take b2 ; :: thesis: ( x = b1 +^ b2 & y = b1 )

thus x = b1 +^ b2 by A167; :: thesis: y = b1

thus y = b1 ; :: thesis: verum

A168: for b being Element of Bags (o1 +^ o2) holds S

A169: for x being Element of Bags o1 ex y being Element of (Polynom-Ring (o2,L)) st S

proof

consider g being Function of (Bags o1), the carrier of (Polynom-Ring (o2,L)) such that
defpred S_{4}[ 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: ex y being Element of (Polynom-Ring (o2,L)) st S_{3}[x,y]

reconsider b1 = x as Element of Bags o1 ;

defpred S_{5}[ 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_{5}[p,q]

A171: for b2 being Element of Bags o2 holds S_{5}[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_{4}[x,y]

A174: for b being Element of Bags (o1 +^ o2) holds S_{4}[b,kk . b]
from FUNCT_2:sch 3(A172);

Support t c= kk .: (Support s)

then reconsider t99 = t as Element of (Polynom-Ring (o2,L)) by POLYNOM1:def 11;

reconsider t9 = t as Function ;

take t99 ; :: thesis: S_{3}[x,t99]

take t9 ; :: thesis: ( t9 = t99 & ( for b2 being Element of Bags o2

for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds

t9 . b2 = s . b ) )

thus t99 = t9 ; :: thesis: for b2 being Element of Bags o2

for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds

t9 . b2 = s . b

let b2 be Element of Bags o2; :: thesis: for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds

t9 . b2 = s . b

let b be Element of Bags (o1 +^ o2); :: thesis: ( b = x +^ b2 implies t9 . b2 = s . b )

assume b = x +^ b2 ; :: thesis: t9 . b2 = s . b

hence t9 . b2 = s . b by A171; :: thesis: verum

end;( $1 = b1 +^ b2 & $2 = b2 );

let x be Element of Bags o1; :: thesis: ex y being Element of (Polynom-Ring (o2,L)) st S

reconsider b1 = x as Element of Bags o1 ;

defpred S

$2 = s . b;

A170: for p being Element of Bags o2 ex q being Element of L st S

proof

consider t being Function of (Bags o2), the carrier of L such that
let p be Element of Bags o2; :: thesis: ex q being Element of L st S_{5}[p,q]

take s . (b1 +^ p) ; :: thesis: S_{5}[p,s . (b1 +^ p)]

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

assume b = b1 +^ p ; :: thesis: s . (b1 +^ p) = s . b

hence s . (b1 +^ p) = s . b ; :: thesis: verum

end;take s . (b1 +^ p) ; :: thesis: S

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

assume b = b1 +^ p ; :: thesis: s . (b1 +^ p) = s . b

hence s . (b1 +^ p) = s . b ; :: thesis: verum

A171: for b2 being Element of Bags o2 holds S

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

proof

consider kk being Function of (Bags (o1 +^ o2)),(Bags o2) such that
let x be Element of Bags (o1 +^ o2); :: thesis: ex y being Element of Bags o2 st S_{4}[x,y]

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: S_{4}[x,y]

take b1 ; :: thesis: ex b2 being Element of Bags o2 st

( x = b1 +^ b2 & y = b2 )

take b2 ; :: thesis: ( x = b1 +^ b2 & y = b2 )

thus x = b1 +^ b2 by A173; :: thesis: y = b2

thus y = b2 ; :: thesis: verum

end;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: S

take b1 ; :: thesis: ex b2 being Element of Bags o2 st

( x = b1 +^ b2 & y = b2 )

take b2 ; :: thesis: ( x = b1 +^ b2 & y = b2 )

thus x = b1 +^ b2 by A173; :: thesis: y = b2

thus y = b2 ; :: thesis: verum

A174: for b being Element of Bags (o1 +^ o2) holds S

Support t c= kk .: (Support s)

proof

then
t is Polynomial of o2,L
by POLYNOM1:def 5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support t or x in kk .: (Support s) )

assume A175: x in Support t ; :: thesis: x in kk .: (Support s)

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

end;assume A175: x in Support t ; :: thesis: x in kk .: (Support s)

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

then reconsider t99 = t as Element of (Polynom-Ring (o2,L)) by POLYNOM1:def 11;

reconsider t9 = t as Function ;

take t99 ; :: thesis: S

take t9 ; :: thesis: ( t9 = t99 & ( for b2 being Element of Bags o2

for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds

t9 . b2 = s . b ) )

thus t99 = t9 ; :: thesis: for b2 being Element of Bags o2

for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds

t9 . b2 = s . b

let b2 be Element of Bags o2; :: thesis: for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds

t9 . b2 = s . b

let b be Element of Bags (o1 +^ o2); :: thesis: ( b = x +^ b2 implies t9 . b2 = s . b )

assume b = x +^ b2 ; :: thesis: t9 . b2 = s . b

hence t9 . b2 = s . b by A171; :: thesis: verum

A177: for x being Element of Bags o1 holds S

reconsider g = g as Function of (Bags o1),(Polynom-Ring (o2,L)) ;

A178: Support g c= kk .: (Support s)

proof

then
g is Polynomial of o1,(Polynom-Ring (o2,L))
by POLYNOM1:def 5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support g or x in kk .: (Support s) )

assume A179: x in Support g ; :: thesis: x in kk .: (Support s)

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

end;assume A179: x in Support g ; :: thesis: x in kk .: (Support s)

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

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: for b being Element of Bags (o1 +^ o2) holds s . b = (Compress g9) . b

then A185: y =
Compress g9
by FUNCT_2:63
let b be Element of Bags (o1 +^ o2); :: thesis: s . b = (Compress g9) . b

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

end;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: verum

.= 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: verum