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

now

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

end;

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