let n be set ; :: thesis: for b, b1, b2 being bag of n st b = b1 + b2 holds
b1 divides b
let b, b1, b2 be bag of n; :: thesis: ( b = b1 + b2 implies b1 divides b )
assume A1: b = b1 + b2 ; :: thesis: b1 divides b
now :: thesis: for k being object st k in n holds
b1 . k <= b . k
let k be object ; :: thesis: ( k in n implies b1 . k <= b . k )
assume k in n ; :: thesis: b1 . k <= b . k
b . k = (b1 . k) + (b2 . k) by A1, Def5;
hence b1 . k <= b . k by NAT_1:11; :: thesis: verum
end;
hence b1 divides b by Th45; :: thesis: verum