let o1, o2 be Ordinal; :: thesis: for b being bag of o1 +^ o2
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 o1 +^ o2; :: 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 ) )
reconsider b' = b as Element of Bags (o1 +^ o2) by PRE_POLY:def 12;
consider c1 being Element of Bags o1, c2 being Element of Bags o2 such that
A1: b' = c1 +^ c2 by Th6;
reconsider c1' = c1, b1' = b1 as bag of o1 ;
reconsider c2' = c2, b2' = b2 as bag of o2 ;
assume A2: 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 )
A3: 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 A4: k in o2 ; :: thesis: c2' . k <= b2' . k
then reconsider k' = k as Ordinal ;
set x = o1 +^ k';
o1 c= o1 +^ k' by ORDINAL3:27;
then A5: not o1 +^ k' in o1 by ORDINAL1:7;
A6: ( (c1 +^ c2) . (o1 +^ k') <= (b1 +^ b2) . (o1 +^ k') & k' = (o1 +^ k') -^ o1 ) by A2, A1, ORDINAL3:65, PRE_POLY:def 11;
o1 +^ k' in o1 +^ o2 by A4, ORDINAL2:49;
then A7: o1 +^ k' in (o1 +^ o2) \ o1 by A5, XBOOLE_0:def 5;
then (b1 +^ b2) . (o1 +^ k') = b2 . ((o1 +^ k') -^ o1) by Def1;
hence c2' . k <= b2' . k by A7, A6, 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 )
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 A8: k in o1 ; :: thesis: c1' . k <= b1' . k
then reconsider k' = k as Ordinal ;
A9: (c1 +^ c2) . k <= (b1 +^ b2) . k by A2, A1, PRE_POLY:def 11;
(c1 +^ c2) . k' = c1 . k' by A8, Def1;
hence c1' . k <= b1' . k by A8, A9, Def1; :: thesis: verum

end;

hence ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 ) by A1, A3, PRE_POLY:46; :: thesis: verum