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:13;
thus (b + (EmptyBag X)) . x = (b . x) + ((EmptyBag X) . x) by Def5
.= b . x by A1 ; :: thesis: verum

end;

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