let o1, o2 be Ordinal; :: thesis: for b being bag of
for b1 being Element of Bags o1
for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
let b be bag of ; :: thesis: for b1 being Element of Bags o1
for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
let b1 be Element of Bags o1; :: thesis: for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
let b2 be Element of Bags o2; :: thesis: ( b divides b1 +^ b2 implies ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 ) )
assume A1: b divides b1 +^ b2 ; :: thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
reconsider b' = b as Element of Bags (o1 +^ o2) by POLYNOM1:def 14;
consider c1 being Element of Bags o1, c2 being Element of Bags o2 such that
A2: b' = c1 +^ c2 by Th6;
reconsider c1' = c1, b1' = b1 as bag of ;
reconsider c2' = c2, b2' = b2 as bag of ;
A3: for k being set st k in o1 holds
c1' . k <= b1' . k

proof

let k be set ; :: thesis: ( k in o1 implies c1' . k <= b1' . k )
assume A4: k in o1 ; :: thesis: c1' . k <= b1' . k
A5: (c1 +^ c2) . k <= (b1 +^ b2) . k by A1, A2, POLYNOM1:def 13;
reconsider k' = k as Ordinal by A4;
(c1 +^ c2) . k' = c1 . k' by A4, Def1;
hence c1' . k <= b1' . k by A4, A5, Def1; :: thesis: verum

end;

A6: for k being set st k in o2 holds
c2' . k <= b2' . k

proof

let k be set ; :: thesis: ( k in o2 implies c2' . k <= b2' . k )
assume A7: k in o2 ; :: thesis: c2' . k <= b2' . k
then reconsider k' = k as Ordinal ;
set x = o1 +^ k';
A8: (c1 +^ c2) . (o1 +^ k') <= (b1 +^ b2) . (o1 +^ k') by A1, A2, POLYNOM1:def 13;
A9: o1 +^ k' in o1 +^ o2 by A7, ORDINAL2:49;
o1 c= o1 +^ k' by ORDINAL3:27;
then not o1 +^ k' in o1 by ORDINAL1:7;
then A10: o1 +^ k' in (o1 +^ o2) \ o1 by A9, XBOOLE_0:def 5;
then A11: (b1 +^ b2) . (o1 +^ k') = b2 . ((o1 +^ k') -^ o1) by Def1;
k' = (o1 +^ k') -^ o1 by ORDINAL3:65;
hence c2' . k <= b2' . k by A8, A10, A11, Def1; :: thesis: verum

end;

take c1 ; :: thesis: ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
take c2 ; :: thesis: ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
thus ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 ) by A2, A3, A6, POLYNOM1:50; :: thesis: verum