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}

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}

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;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

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

o in support (b \ a)

hence
support (b \ a) = (support b) \ {a}
by A, TARSKI:2; :: thesis: verumo 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;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