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

let x be set ; :: thesis: ( x in X implies (b -' (EmptyBag X)) . x = b . x )
assume x in X ; :: thesis: (b -' (EmptyBag X)) . x = b . x
then A1: (EmptyBag X) . x = 0 by FUNCOP_1:7;
thus (b -' (EmptyBag X)) . x = (b . x) -' ((EmptyBag X) . x) by Def6
.= b . x by A1, NAT_D:40 ; :: thesis: verum

end;

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