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

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

hence
b1 +^ b2 divides c1 +^ c2
by PRE_POLY:46; :: thesis: verum(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_{1} <= (c1 +^ c2) . b_{1} )

A3: b19 . k <= c19 . k by A1, PRE_POLY:def 11;

assume A4: k in o1 +^ o2 ; :: thesis: (b1 +^ b2) . b_{1} <= (c1 +^ c2) . b_{1}

end;let k be object ; :: thesis: ( k in o1 +^ o2 implies (b1 +^ b2) . b

A3: b19 . k <= c19 . k by A1, PRE_POLY:def 11;

assume A4: k in o1 +^ o2 ; :: thesis: (b1 +^ b2) . b