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} )
A: now :: thesis: ( b is zero implies rng b = {0} )
assume B: b is zero ; :: thesis: rng b = {0}
C: now :: thesis: for o being object st o in rng b holds
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;
now :: thesis: for o being object st o in {0} holds
o 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;
hence rng b = {0} by C, TARSKI:2; :: thesis: verum
end;
now :: thesis: ( rng b = {0} implies b is zero )
assume B: rng b = {0} ; :: 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 B, TARSKI:def 1; :: thesis: verum
end;
hence b is zero by PBOOLE:6; :: thesis: verum
end;
hence ( b is zero iff rng b = {0} ) by A; :: thesis: verum