let X be set ; :: thesis: for b1, b2 being bag of X holds (b2 + b1) -' b1 = b2
let b1, b2 be bag of X; :: thesis: (b2 + b1) -' b1 = b2

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

let k be object ; :: thesis: ( k in X implies ((b2 + b1) -' b1) . k = b2 . k )
assume k in X ; :: thesis: ((b2 + b1) -' b1) . k = b2 . k
thus ((b2 + b1) -' b1) . k = ((b2 + b1) . k) -' (b1 . k) by Def6
.= ((b2 . k) + (b1 . k)) -' (b1 . k) by Def5
.= b2 . k by NAT_D:34 ; :: thesis: verum

end;

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