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
proof
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;
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 object st k in o1 holds
c19 . k <= b19 . k
proof
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;
hence ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 ) by A1, A3, PRE_POLY:46; :: thesis: verum