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

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