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

A: now :: thesis: for o being object st o in support (b \ a) holds
o in (support b) \ {a}

let o be object ; :: thesis: ( o in support (b \ a) implies o in (support b) \ {a} )
assume X: o in support (b \ a) ; :: thesis: o in (support b) \ {a}
then reconsider c = o as Element of X ;
B: (b \ a) . o <> 0 by X, PRE_POLY:def 7;
then D: a <> o by bb1;
then b . c = (b \ a) . c by FUNCT_7:32;
then C: o in support b by B, PRE_POLY:def 7;
not o in {a} by D, TARSKI:def 1;
hence o in (support b) \ {a} by C, XBOOLE_0:def 5; :: thesis: verum

end;

now :: thesis: for o being object st o in (support b) \ {a} holds
o in support (b \ a)

let o be object ; :: thesis: ( o in (support b) \ {a} implies o in support (b \ a) )
assume X: o in (support b) \ {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 X, XBOOLE_0:def 5;
then o <> a by TARSKI:def 1;
then (b \ a) . c = b . c by FUNCT_7:32;
then (b \ a) . o <> 0 by B, PRE_POLY:def 7;
hence o in support (b \ a) by PRE_POLY:def 7; :: thesis: verum

end;

hence support (b \ a) = (support b) \ {a} by A, TARSKI:2; :: thesis: verum