let X be non empty set ; :: thesis:
let b be bag of X; :: thesis:
let a be Element of X; :: thesis:

A: now :: thesis:

let o be object ; :: thesis:
assume X: o in support (b \ a) ; :: thesis:
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:

end;

let o be object ; :: thesis:
assume X: o in (support b) \ {a} ; :: thesis:
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:

end;

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