let X be non empty set ; :: thesis: for b being bag of X
for a being Element of X holds (b \ a) . a = 0
let b be bag of X; :: thesis: for a being Element of X holds (b \ a) . a = 0
let a be Element of X; :: thesis: (b \ a) . a = 0
X = dom b by PARTFUN1:def 2;
hence (b \ a) . a = 0 by FUNCT_7:31; :: thesis: verum