let X be non empty set ; :: thesis: for b being bag of X holds
( b is zero iff rng b = )

let b be bag of X; :: thesis: ( b is zero iff rng b = )
A: now :: thesis: ( b is zero implies rng b = )
assume B: b is zero ; :: thesis:
C: now :: thesis: for o being object st o in rng b holds
o in
let o be object ; :: thesis: ( o in rng b implies o in )
assume o in rng b ; :: thesis:
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 by TARSKI:def 1; :: thesis: verum
end;
now :: thesis: for o being object st o in holds
o in rng b
let o be object ; :: thesis: ( o in implies o in rng b )
assume o in ; :: 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 ; :: thesis: verum
end;
hence rng b = by ; :: thesis: verum
end;
now :: thesis: ( rng b = implies b is zero )
assume B: rng b = ; :: thesis: b is zero
now :: thesis: for o being object st o in X holds
b . 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 ; :: thesis: verum
end;
hence b is zero by PBOOLE:6; :: thesis: verum
end;
hence ( b is zero iff rng b = ) by A; :: thesis: verum