let X be set ; :: thesis: for b being bag of X holds 0 (#) b = EmptyBag X
let b be bag of X; :: thesis: 0 (#) b = EmptyBag X
set E = EmptyBag X;
A1: ( dom (0 (#) b) = X & X = dom (EmptyBag X) & X = dom b ) by PARTFUN1:def 2;
for x being object st x in dom (EmptyBag X) holds
(EmptyBag X) . x = (0 (#) b) . x

proof

let x be object ; :: thesis: ( x in dom (EmptyBag X) implies (EmptyBag X) . x = (0 (#) b) . x )
(0 (#) b) . x = 0 * (b . x) by VALUED_1:6;
hence ( x in dom (EmptyBag X) implies (EmptyBag X) . x = (0 (#) b) . x ) ; :: thesis: verum

end;

hence 0 (#) b = EmptyBag X by A1; :: thesis: verum