let X be non empty set ; :: thesis: for b being bag of X holds

( b is zero iff support b = {} )

let b be bag of X; :: thesis: ( b is zero iff support b = {} )

( b is zero iff support b = {} )

let b be bag of X; :: thesis: ( b is zero iff support b = {} )

now :: thesis: ( support b = {} implies b is zero )

hence
( b is zero iff support b = {} )
; :: thesis: verumassume
support b = {}
; :: thesis: b is zero

then for o being object st o in X holds

b . o = {} by PRE_POLY:def 7;

hence b is zero by PBOOLE:6; :: thesis: verum

end;then for o being object st o in X holds

b . o = {} by PRE_POLY:def 7;

hence b is zero by PBOOLE:6; :: thesis: verum