let X be non empty set ; :: thesis: for b being bag of X
for a being Element of X holds
( b \ a = b iff not a in support b )

let b be bag of X; :: thesis: for a being Element of X holds
( b \ a = b iff not a in support b )

let a be Element of X; :: thesis: ( b \ a = b iff not a in support b )
A: now :: thesis: ( not a in support b implies b \ a = b )
assume B: not a in support b ; :: thesis: b \ a = b
now :: thesis: for o being object st o in X holds
(b \ a) . o = b . o
let o be object ; :: thesis: ( o in X implies (b \ a) . b1 = b . b1 )
assume o in X ; :: thesis: (b \ a) . b1 = b . b1
per cases ( o = a or o <> a ) ;
suppose D: o = a ; :: thesis: (b \ a) . b1 = b . b1
hence (b \ a) . o = 0 by bb1
.= b . o by ;
:: thesis: verum
end;
suppose o <> a ; :: thesis: (b \ a) . b1 = b . b1
hence (b \ a) . o = b . o by FUNCT_7:32; :: thesis: verum
end;
end;
end;
hence b \ a = b by PBOOLE:3; :: thesis: verum
end;
now :: thesis: ( b \ a = b implies not a in support b )end;
hence ( b \ a = b iff not a in support b ) by A; :: thesis: verum