let n be set ; :: thesis: for b1, b2 being bag of n st b1 divides b2 holds
(b2 -' b1) + b1 = b2
let b1, b2 be bag of n; :: thesis: ( b1 divides b2 implies (b2 -' b1) + b1 = b2 )
assume A1: b1 divides b2 ; :: thesis: (b2 -' b1) + b1 = b2

now :: thesis: for k being object st k in n holds
((b2 -' b1) + b1) . k = b2 . k

let k be object ; :: thesis: ( k in n implies ((b2 -' b1) + b1) . k = b2 . k )
assume k in n ; :: thesis: ((b2 -' b1) + b1) . k = b2 . k
A2: b1 . k <= b2 . k by A1;
thus ((b2 -' b1) + b1) . k = ((b2 -' b1) . k) + (b1 . k) by Def5
.= ((b2 . k) -' (b1 . k)) + (b1 . k) by Def6
.= ((b2 . k) + (b1 . k)) -' (b1 . k) by A2, NAT_D:38
.= b2 . k by NAT_D:34 ; :: thesis: verum

end;

hence (b2 -' b1) + b1 = b2 ; :: thesis: verum