deffunc H1( 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 S1[ 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 = { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } ;
A1: for B being set st B in { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } holds
B is finite
proof
let B be set ; :: thesis: ( B in { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } implies B is finite )
assume B in { H1(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 H2( 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 = { H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } ;
A3: B c= { H2(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 { H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } )
assume x in B ; :: thesis: x in { H2(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 { H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } ; :: thesis: verum
end;
A4: Support Q0 is finite ;
{ H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0 } is finite from 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 S1[b,u]
proof
let b be Element of Bags (o1 +^ o2); :: thesis: ex u being Element of L st S1[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: S1[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 S1[b,f . b] from reconsider f = f as Series of (o1 +^ o2),L ;
A8: Support f = union { H1(b1) where b1 is Element of Bags o1 : b1 in Support P }
proof
thus Support f c= union { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } :: according to XBOOLE_0:def 10 :: thesis: union { H1(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 { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } )
assume A9: x in Support f ; :: thesis: x in union { H1(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 ;
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 ;
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 ;
hence contradiction by A10, A11, A15, POLYNOM1:22; :: thesis: verum
end;
then b1 in Support P by POLYNOM1:def 4;
then A17: Y in { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } by A12;
b2 = b29 by ;
then b2 in Support Q1 by ;
then x in Y by A11, A12, A13, A16;
hence x in union { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } or x in Support f )
assume x in union { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } ; :: thesis:
then consider Y being set such that
A18: x in Y and
A19: Y in { H1(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 ;
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 ;
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 ;
Q1 = Q by A23, A26, A27, Th7;
hence x in Support f by ; :: thesis: verum
end;
A30: Support P is finite by POLYNOM1:def 5;
{ H1(b1) where b1 is Element of Bags o1 : b1 in Support P } is finite from then union { H1(b1) where b1 is Element of Bags o1 : b1 in Support P } is finite by ;
then reconsider f = f as Polynomial of (o1 +^ o2),L by ;
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 ;
hence f . b = Q1 . b2 by A34, A31, A32, A33, Th7; :: thesis: verum