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 ) } ;
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 );
set A = { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } ;
A1: 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
A2: 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 ;
deffunc H₂( Element of Bags o2) -> Element of Bags (o1 +^ o2) = b1 +^ $1;
reconsider Q0 = P . b1 as Polynomial of o2,L by POLYNOM1:def 11;
set B0 = { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } ;
A3: B c= { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 }

proof

let x be object ; :: 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 ex b2 being Element of Bags o2 st
( x = b1 +^ b2 & ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) ) by A2;
hence x in { H₂(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } ; :: thesis: verum

end;

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

end;

A5: 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
A6: b = b1 +^ b2 by Th6;
reconsider Q1 = P . b1 as Polynomial of o2,L by POLYNOM1:def 11;
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 A6; :: thesis: verum

end;

consider f being Function of (Bags (o1 +^ o2)), the carrier of L such that
A7: for b being Element of Bags (o1 +^ o2) holds S₁[b,f . b] from FUNCT_2:sch 3(A5);
reconsider f = f as Series of (o1 +^ o2),L ;
A8: 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 object ; :: 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 A9: x in Support f ; :: thesis: x in union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P }
then A10: f . x <> 0. L by POLYNOM1:def 4;
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A11: x = b1 +^ b2 by A9, Th6;
consider Y being set such that
A12: Y = { (b1 +^ b29) where b29 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . b1 & b29 in Support Q ) } ;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A13: Q1 = P . b19 and
A14: b1 +^ b2 = b19 +^ b29 and
A15: f . (b1 +^ b2) = Q1 . b29 by A7;
A16: b1 = b19 by A14, Th7;

now :: thesis: not P . b1 = 0. (Polynom-Ring (o2,L))

assume P . b1 = 0. (Polynom-Ring (o2,L)) ; :: thesis: contradiction
then Q1 = 0_ (o2,L) by A13, A16, POLYNOM1:def 11;
hence contradiction by A10, A11, A15, POLYNOM1:22; :: thesis: verum

end;

then b1 in Support P by POLYNOM1:def 4;
then A17: Y in { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } by A12;
b2 = b29 by A14, Th7;
then b2 in Support Q1 by A10, A11, A15, POLYNOM1:def 4;
then x in Y by A11, A12, A13, A16;
hence x in union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } by A17, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: 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
A18: x in Y and
A19: 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
A20: 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 A19;
consider b2 being Element of Bags o2 such that
A21: x = b1 +^ b2 and
A22: ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) by A18, A20;
consider Q being Polynomial of o2,L such that
A23: Q = P . b1 and
A24: b2 in Support Q by A22;
A25: Q . b2 <> 0. L by A24, POLYNOM1:def 4;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A26: Q1 = P . b19 and
A27: b1 +^ b2 = b19 +^ b29 and
A28: f . (b1 +^ b2) = Q1 . b29 by A7;
A29: f . (b1 +^ b2) = Q1 . b2 by A27, A28, Th7;
Q1 = Q by A23, A26, A27, Th7;
hence x in Support f by A21, A25, A29, POLYNOM1:def 4; :: thesis: verum

end;

A30: Support P is finite by POLYNOM1:def 5;
{ H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } is finite from FRAENKEL:sch 21(A30);
then union { H₁(b1) where b1 is Element of Bags o1 : b1 in Support P } is finite by A1, FINSET_1:7;
then reconsider f = f as Polynomial of (o1 +^ o2),L by A8, POLYNOM1:def 5;
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 b19 being Element of Bags o1, b29 being Element of Bags o2, Q19 being Polynomial of o2,L such that
A31: Q19 = P . b19 and
A32: b = b19 +^ b29 and
A33: f . b = Q19 . b29 by A7;
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A34: b = b1 +^ b2 by Th6;
reconsider Q1 = P . b1 as Polynomial of o2,L by POLYNOM1:def 11;
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 )
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 A34; :: thesis: f . b = Q1 . b2
b1 = b19 by A34, A32, Th7;
hence f . b = Q1 . b2 by A34, A31, A32, A33, Th7; :: thesis: verum