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 A1: ( b1 divides c1 & b2 divides c2 ) ; :: thesis: b1 +^ b2 divides c1 +^ c2

now

let k be set ; :: thesis: ( k in o1 +^ o2 implies (b1 +^ b2) . b₁ <= (c1 +^ c2) . b₁ )
assume A2: k in o1 +^ o2 ; :: thesis: (b1 +^ b2) . b₁ <= (c1 +^ c2) . b₁
reconsider b1' = b1, c1' = c1 as bag of ;
A3: b1' . k <= c1' . k by A1, POLYNOM1:def 13;

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

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

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

end;

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

then reconsider k' = k as Ordinal ;
A6: (b1 +^ b2) . k' = b2 . (k' -^ o1) by A5, Def1;
(c1 +^ c2) . k' = c2 . (k' -^ o1) by A5, Def1;
hence (b1 +^ b2) . k <= (c1 +^ c2) . k by A1, A6, POLYNOM1:def 13; :: thesis: verum

end;

end;

end;

hence b1 +^ b2 divides c1 +^ c2 by POLYNOM1:50; :: thesis: verum