let X be set ; :: thesis: for b being bag of X holds b -' (EmptyBag X) = b
let b be bag of X; :: thesis: b -' (EmptyBag X) = b

now :: thesis: for x being object st x in X holds
(b -' (EmptyBag X)) . x = b . x

let x be object ; :: thesis: ( x in X implies (b -' (EmptyBag X)) . x = b . x )
assume x in X ; :: thesis: (b -' (EmptyBag X)) . x = b . x
thus (b -' (EmptyBag X)) . x = (b . x) -' ((EmptyBag X) . x) by Def6
.= b . x by NAT_D:40 ; :: thesis: verum

end;

hence b -' (EmptyBag X) = b ; :: thesis: verum