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) . b₁ = b . b₁ )
assume o in X ; :: thesis: (b \ a) . b₁ = b . b₁

per cases ( o = a or o <> a ) ;

suppose D: o = a ; :: thesis: (b \ a) . b₁ = b . b₁

hence (b \ a) . o = 0 by bb1
.= b . o by B, D, PRE_POLY:def 7 ;
:: thesis: verum

end;

suppose o <> a ; :: thesis: (b \ a) . b₁ = b . b₁

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 )

assume b \ a = b ; :: thesis: not a in support b
then b . a = 0 by bb1;
hence not a in support b by PRE_POLY:def 7; :: thesis: verum

end;

hence ( b \ a = b iff not a in support b ) by A; :: thesis: verum