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 b9 = 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: b9 = c1 +^ c2 by Th6;

reconsider c19 = c1, b19 = b1 as bag of o1 ;

reconsider c29 = c2, b29 = 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 object st k in o2 holds

c29 . k <= b29 . k

( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )

take c2 ; :: thesis: ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )

for k being object st k in o1 holds

c19 . k <= b19 . k

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 b9 = 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: b9 = c1 +^ c2 by Th6;

reconsider c19 = c1, b19 = b1 as bag of o1 ;

reconsider c29 = c2, b29 = 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 object st k in o2 holds

c29 . k <= b29 . k

proof

take
c1
; :: thesis: ex c2 being Element of Bags o2 st
let k be object ; :: thesis: ( k in o2 implies c29 . k <= b29 . k )

assume A4: k in o2 ; :: thesis: c29 . k <= b29 . k

then reconsider k9 = k as Ordinal ;

set x = o1 +^ k9;

o1 c= o1 +^ k9 by ORDINAL3:24;

then A5: not o1 +^ k9 in o1 by ORDINAL1:5;

A6: ( (c1 +^ c2) . (o1 +^ k9) <= (b1 +^ b2) . (o1 +^ k9) & k9 = (o1 +^ k9) -^ o1 ) by A2, A1, ORDINAL3:52, PRE_POLY:def 11;

o1 +^ k9 in o1 +^ o2 by A4, ORDINAL2:32;

then A7: o1 +^ k9 in (o1 +^ o2) \ o1 by A5, XBOOLE_0:def 5;

then (b1 +^ b2) . (o1 +^ k9) = b2 . ((o1 +^ k9) -^ o1) by Def1;

hence c29 . k <= b29 . k by A7, A6, Def1; :: thesis: verum

end;assume A4: k in o2 ; :: thesis: c29 . k <= b29 . k

then reconsider k9 = k as Ordinal ;

set x = o1 +^ k9;

o1 c= o1 +^ k9 by ORDINAL3:24;

then A5: not o1 +^ k9 in o1 by ORDINAL1:5;

A6: ( (c1 +^ c2) . (o1 +^ k9) <= (b1 +^ b2) . (o1 +^ k9) & k9 = (o1 +^ k9) -^ o1 ) by A2, A1, ORDINAL3:52, PRE_POLY:def 11;

o1 +^ k9 in o1 +^ o2 by A4, ORDINAL2:32;

then A7: o1 +^ k9 in (o1 +^ o2) \ o1 by A5, XBOOLE_0:def 5;

then (b1 +^ b2) . (o1 +^ k9) = b2 . ((o1 +^ k9) -^ o1) by Def1;

hence c29 . k <= b29 . k by A7, A6, Def1; :: thesis: verum

( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )

take c2 ; :: thesis: ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )

for k being object st k in o1 holds

c19 . k <= b19 . k

proof

hence
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
by A1, A3, PRE_POLY:46; :: thesis: verum
let k be object ; :: thesis: ( k in o1 implies c19 . k <= b19 . k )

assume A8: k in o1 ; :: thesis: c19 . k <= b19 . k

then reconsider k9 = k as Ordinal ;

A9: (c1 +^ c2) . k <= (b1 +^ b2) . k by A2, A1, PRE_POLY:def 11;

(c1 +^ c2) . k9 = c1 . k9 by A8, Def1;

hence c19 . k <= b19 . k by A8, A9, Def1; :: thesis: verum

end;assume A8: k in o1 ; :: thesis: c19 . k <= b19 . k

then reconsider k9 = k as Ordinal ;

A9: (c1 +^ c2) . k <= (b1 +^ b2) . k by A2, A1, PRE_POLY:def 11;

(c1 +^ c2) . k9 = c1 . k9 by A8, Def1;

hence c19 . k <= b19 . k by A8, A9, Def1; :: thesis: verum