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

let b be bag of X; :: thesis: for a being Element of X holds support (b \ a) = () \ {a}
let a be Element of X; :: thesis: support (b \ a) = () \ {a}
A: now :: thesis: for o being object st o in support (b \ a) holds
o in () \ {a}
let o be object ; :: thesis: ( o in support (b \ a) implies o in () \ {a} )
assume X: o in support (b \ a) ; :: thesis: o in () \ {a}
then reconsider c = o as Element of X ;
B: (b \ a) . o <> 0 by ;
then D: a <> o by bb1;
then b . c = (b \ a) . c by FUNCT_7:32;
then C: o in support b by ;
not o in {a} by ;
hence o in () \ {a} by ; :: thesis: verum
end;
now :: thesis: for o being object st o in () \ {a} holds
o in support (b \ a)
let o be object ; :: thesis: ( o in () \ {a} implies o in support (b \ a) )
assume X: o in () \ {a} ; :: thesis: o in support (b \ a)
then reconsider c = o as Element of X ;
B: ( o in support b & not o in {a} ) by ;
then o <> a by TARSKI:def 1;
then (b \ a) . c = b . c by FUNCT_7:32;
then (b \ a) . o <> 0 by ;
hence o in support (b \ a) by PRE_POLY:def 7; :: thesis: verum
end;
hence support (b \ a) = () \ {a} by ; :: thesis: verum