let o1, o2 be Ordinal; :: thesis: for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 divides c1 & b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2
let b1, c1 be Element of Bags o1; :: thesis: for b2, c2 being Element of Bags o2 st b1 divides c1 & b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2
let b2, c2 be Element of Bags o2; :: thesis: ( b1 divides c1 & b2 divides c2 implies b1 +^ b2 divides c1 +^ c2 )
assume that
A1: b1 divides c1 and
A2: b2 divides c2 ; :: thesis: b1 +^ b2 divides c1 +^ c2

now :: thesis: for k being object st k in o1 +^ o2 holds
(b1 +^ b2) . k <= (c1 +^ c2) . k

reconsider b19 = b1, c19 = c1 as bag of o1 ;
let k be object ; :: thesis: ( k in o1 +^ o2 implies (b1 +^ b2) . b₁ <= (c1 +^ c2) . b₁ )
A3: b19 . k <= c19 . k by A1, PRE_POLY:def 11;
assume A4: k in o1 +^ o2 ; :: thesis: (b1 +^ b2) . b₁ <= (c1 +^ c2) . b₁

per cases ( k in o1 or k in (o1 +^ o2) \ o1 ) by A4, XBOOLE_0:def 5;

suppose A5: k in o1 ; :: thesis: (b1 +^ b2) . b₁ <= (c1 +^ c2) . b₁

then reconsider k9 = k as Ordinal ;
(b1 +^ b2) . k9 = b1 . k9 by A5, Def1;
hence (b1 +^ b2) . k <= (c1 +^ c2) . k by A3, A5, Def1; :: thesis: verum

end;

suppose A6: k in (o1 +^ o2) \ o1 ; :: thesis: (b1 +^ b2) . b₁ <= (c1 +^ c2) . b₁

then reconsider k9 = k as Ordinal ;
( (b1 +^ b2) . k9 = b2 . (k9 -^ o1) & (c1 +^ c2) . k9 = c2 . (k9 -^ o1) ) by A6, Def1;
hence (b1 +^ b2) . k <= (c1 +^ c2) . k by A2, PRE_POLY:def 11; :: thesis: verum

end;

end;

end;

hence b1 +^ b2 divides c1 +^ c2 by PRE_POLY:46; :: thesis: verum