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

( b is zero iff rng b = {0} )

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

( b is zero iff rng b = {0} )

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

A: now :: thesis: ( b is zero implies rng b = {0} )

assume B:
b is zero
; :: thesis: rng b = {0}

end;C: now :: thesis: for o being object st o in rng b holds

o in {0}

o in {0}

let o be object ; :: thesis: ( o in rng b implies o in {0} )

assume o in rng b ; :: thesis: o in {0}

then consider y being object such that

D: ( y in dom b & b . y = o ) by FUNCT_1:def 3;

o = 0 by B, D;

hence o in {0} by TARSKI:def 1; :: thesis: verum

end;assume o in rng b ; :: thesis: o in {0}

then consider y being object such that

D: ( y in dom b & b . y = o ) by FUNCT_1:def 3;

o = 0 by B, D;

hence o in {0} by TARSKI:def 1; :: thesis: verum

now :: thesis: for o being object st o in {0} holds

o in rng b

hence
rng b = {0}
by C, TARSKI:2; :: thesis: verumo in rng b

let o be object ; :: thesis: ( o in {0} implies o in rng b )

assume o in {0} ; :: thesis: o in rng b

then D: o = 0 by TARSKI:def 1;

set y = the Element of X;

E: dom b = X by PARTFUN1:def 2;

b . the Element of X = 0 by B;

hence o in rng b by D, E, FUNCT_1:def 3; :: thesis: verum

end;assume o in {0} ; :: thesis: o in rng b

then D: o = 0 by TARSKI:def 1;

set y = the Element of X;

E: dom b = X by PARTFUN1:def 2;

b . the Element of X = 0 by B;

hence o in rng b by D, E, FUNCT_1:def 3; :: thesis: verum

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

hence
( b is zero iff rng b = {0} )
by A; :: thesis: verumassume B:
rng b = {0}
; :: thesis: b is zero

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

b . o = {}

hence
b is zero
by PBOOLE:6; :: thesis: verumb . o = {}

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

assume o in X ; :: thesis: b . o = {}

then o in dom b by PARTFUN1:def 2;

then b . o in rng b by FUNCT_1:3;

hence b . o = {} by B, TARSKI:def 1; :: thesis: verum

end;assume o in X ; :: thesis: b . o = {}

then o in dom b by PARTFUN1:def 2;

then b . o in rng b by FUNCT_1:3;

hence b . o = {} by B, TARSKI:def 1; :: thesis: verum