deffunc H_{1}( 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_{1}[ 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_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P } ;

A1: for B being set st B in { H_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P } holds

B is finite_{1}[b,u]

A7: for b being Element of Bags (o1 +^ o2) holds S_{1}[b,f . b]
from FUNCT_2:sch 3(A5);

reconsider f = f as Series of (o1 +^ o2),L ;

A8: Support f = union { H_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P }

{ H_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P } is finite
from FRAENKEL:sch 21(A30);

then union { H_{1}(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

( Q = P . $1 & b2 in Support Q ) } ;

defpred S

( Q1 = P . b1 & $1 = b1 +^ b2 & $2 = Q1 . b2 );

set A = { H

A1: for B being set st B in { H

B is finite

proof

A5:
for b being Element of Bags (o1 +^ o2) ex u being Element of L st S
let B be set ; :: thesis: ( B in { H_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P } implies B is finite )

assume B in { H_{1}(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_{2}( 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_{2}(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } ;

A3: B c= { H_{2}(b2) where b2 is Element of Bags o2 : b2 in Support Q0 }

{ H_{2}(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;assume B in { H

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

reconsider Q0 = P . b1 as Polynomial of o2,L by POLYNOM1:def 11;

set B0 = { H

A3: B c= { H

proof

A4:
Support Q0 is finite
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in { H_{2}(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } )

assume x in B ; :: thesis: x in { H_{2}(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_{2}(b2) where b2 is Element of Bags o2 : b2 in Support Q0 }
; :: thesis: verum

end;assume x in B ; :: thesis: x in { H

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

{ H

hence B is finite by A3; :: thesis: verum

proof

consider f being Function of (Bags (o1 +^ o2)), the carrier of L such that
let b be Element of Bags (o1 +^ o2); :: thesis: ex u being Element of L st S_{1}[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_{1}[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 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

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

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

reconsider f = f as Series of (o1 +^ o2),L ;

A8: Support f = union { H

proof

A30:
Support P is finite
by POLYNOM1:def 5;
thus
Support f c= union { H_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P }
:: according to XBOOLE_0:def 10 :: thesis: union { H_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P } c= Support f_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P } or x in Support f )

assume x in union { H_{1}(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_{1}(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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support f or x in union { H_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P } )

assume A9: x in Support f ; :: thesis: x in union { H_{1}(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;

then A17: Y in { H_{1}(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_{1}(b1) where b1 is Element of Bags o1 : b1 in Support P }
by A17, TARSKI:def 4; :: thesis: verum

end;assume A9: x in Support f ; :: thesis: x in union { H

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

then
b1 in Support P
by POLYNOM1:def 4;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 Q1 = 0_ (o2,L) by A13, A16, POLYNOM1:def 11;

hence contradiction by A10, A11, A15, POLYNOM1:22; :: thesis: verum

then A17: Y in { H

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

assume x in union { H

then consider Y being set such that

A18: x in Y and

A19: Y in { H

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

{ H

then union { H

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