defpred S₁[ Element of Bags (o1 +^ o2), Element of L] means ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & $1 = b1 +^ b2 & $2 = Q1 . b2 );
A1: for b being Element of Bags (o1 +^ o2) ex u being Element of L st S₁[b,u]

proof

let b be Element of Bags (o1 +^ o2); :: thesis: ex u being Element of L st S₁[b,u]
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A2: b = b1 +^ b2 by Th6;
reconsider Q1 = P . b1 as Polynomial of o2,L by POLYNOM1:def 27;
take Q1 . b2 ; :: thesis: S₁[b,Q1 . b2]
take b1 ; :: thesis: ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 )
take b2 ; :: thesis: ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 )
take Q1 ; :: thesis: ( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 )
thus ( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 ) by A2; :: thesis: verum

end;

consider f being Function of (Bags (o1 +^ o2)),the carrier of L such that
A3: for b being Element of Bags (o1 +^ o2) holds S₁[b,f . b] from FUNCT_2:sch 3(A1);
reconsider f = f as Series of (o1 +^ o2),L ;
deffunc H₁( Element of Bags o1) -> set = { ($1 +^ b2) where b2 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . $1 & b2 in Support Q ) } ;
set A = { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } ;
A4: Support P is finite by POLYNOM1:def 10;
A5: { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } is finite from FRAENKEL:sch 21(A4);
for B being set st B in { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } holds
B is finite

proof

let B be set ; :: thesis: ( B in { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } implies B is finite )
assume B in { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } ; :: thesis: B is finite
then consider b1 being Element of Bags o1 such that
A6: B = { (b1 +^ b2) where b2 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) } and
b1 in Support P ;
reconsider Q0 = P . b1 as Polynomial of o2,L by POLYNOM1:def 27;
deffunc H₂( Element of Bags o2) -> Element of Bags (o1 +^ o2) = b1 +^ $1;
set B0 = { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } ;
A7: B = { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 }

proof

thus B c= { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } :: according to XBOOLE_0:def 10 :: thesis: { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } )
assume x in B ; :: thesis: x in { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 }
then consider b2 being Element of Bags o2 such that
A8: x = b1 +^ b2 and
A9: ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) by A6;
consider Q being Polynomial of o2,L such that
A10: Q = P . b1 and
A11: b2 in Support Q by A9;
thus x in { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } by A8, A10, A11; :: thesis: verum

end;

thus { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } c= B :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } or x in B )
assume x in { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } ; :: thesis: x in B
then consider b2 being Element of Bags o2 such that
A12: x = b1 +^ b2 and
A13: b2 in Support Q0 ;
thus x in B by A6, A12, A13; :: thesis: verum

end;

end;

A14: Support Q0 is finite ;
{ H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } is finite from FRAENKEL:sch 21(A14);
hence B is finite by A7; :: thesis: verum

end;

then A15: union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } is finite by A5, FINSET_1:25;
Support f = union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P }

proof

thus Support f c= union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } :: according to XBOOLE_0:def 10 :: thesis: union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } c= Support f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Support f or x in union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } )
assume A16: x in Support f ; :: thesis: x in union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P }
then A17: f . x <> 0. L by POLYNOM1:def 9;
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A18: x = b1 +^ b2 by A16, Th6;
consider Y being set such that
A19: Y = { (b1 +^ b2') where b2' is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . b1 & b2' in Support Q ) } ;
consider b1' being Element of Bags o1, b2' being Element of Bags o2, Q1 being Polynomial of o2,L such that
A20: Q1 = P . b1' and
A21: b1 +^ b2 = b1' +^ b2' and
A22: f . (b1 +^ b2) = Q1 . b2' by A3;
A23: ( b1 = b1' & b2 = b2' ) by A21, Th7;
then b2 in Support Q1 by A17, A18, A22, POLYNOM1:def 9;
then A24: x in Y by A18, A19, A20, A23;

now

assume P . b1 = 0. (Polynom-Ring o2,L) ; :: thesis: contradiction
then Q1 = 0_ o2,L by A20, A23, POLYNOM1:def 27;
hence contradiction by A17, A18, A22, POLYNOM1:81; :: thesis: verum

end;

then b1 in Support P by POLYNOM1:def 9;
then Y in { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } by A19;
hence x in union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } by A24, TARSKI:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } or x in Support f )
assume x in union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } ; :: thesis: x in Support f
then consider Y being set such that
A25: x in Y and
A26: Y in { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } by TARSKI:def 4;
consider b1 being Element of Bags o1 such that
A27: Y = { (b1 +^ b2) where b2 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) } and
b1 in Support P by A26;
consider b2 being Element of Bags o2 such that
A28: x = b1 +^ b2 and
A29: ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) by A25, A27;
consider Q being Polynomial of o2,L such that
A30: Q = P . b1 and
A31: b2 in Support Q by A29;
A32: Q . b2 <> 0. L by A31, POLYNOM1:def 9;
consider b1' being Element of Bags o1, b2' being Element of Bags o2, Q1 being Polynomial of o2,L such that
A33: Q1 = P . b1' and
A34: b1 +^ b2 = b1' +^ b2' and
A35: f . (b1 +^ b2) = Q1 . b2' by A3;
A36: Q1 = Q by A30, A33, A34, Th7;
f . (b1 +^ b2) = Q1 . b2 by A34, A35, Th7;
hence x in Support f by A28, A32, A36, POLYNOM1:def 9; :: thesis: verum

end;

then reconsider f = f as Polynomial of (o1 +^ o2),L by A15, POLYNOM1:def 10;
take f ; :: thesis: for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
let b be Element of Bags (o1 +^ o2); :: thesis: ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A37: b = b1 +^ b2 by Th6;
take b1 ; :: thesis: ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
take b2 ; :: thesis: ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
reconsider Q1 = P . b1 as Polynomial of o2,L by POLYNOM1:def 27;
take Q1 ; :: thesis: ( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
thus Q1 = P . b1 ; :: thesis: ( b = b1 +^ b2 & f . b = Q1 . b2 )
thus b = b1 +^ b2 by A37; :: thesis: f . b = Q1 . b2
consider b1' being Element of Bags o1, b2' being Element of Bags o2, Q1' being Polynomial of o2,L such that
A38: Q1' = P . b1' and
A39: b = b1' +^ b2' and
A40: f . b = Q1' . b2' by A3;
( b1 = b1' & b2 = b2' ) by A37, A39, Th7;
hence f . b = Q1 . b2 by A38, A40; :: thesis: verum