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 )

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

end;now :: thesis: for o being object st o in X holds

(b \ a) . o = b . o

hence
b \ a = b
by PBOOLE:3; :: thesis: verum(b \ a) . o = b . o

let o be object ; :: thesis: ( o in X implies (b \ a) . b_{1} = b . b_{1} )

assume o in X ; :: thesis: (b \ a) . b_{1} = b . b_{1}

end;assume o in X ; :: thesis: (b \ a) . b

now :: thesis: ( b \ a = b implies not a in support b )

hence
( b \ a = b iff not a in support b )
by A; :: thesis: verumassume
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;then b . a = 0 by bb1;

hence not a in support b by PRE_POLY:def 7; :: thesis: verum