let X be set ; :: thesis: chi (X,X) is positive-yielding

now :: thesis: for r being Real st r in rng (chi (X,X)) holds
0 < r

let r be Real; :: thesis: ( r in rng (chi (X,X)) implies 0 < r )
assume A1: r in rng (chi (X,X)) ; :: thesis: 0 < r
r <> 0

proof

assume A2: r = 0 ; :: thesis: contradiction
ex s being Element of X st
( s in dom (chi (X,X)) & r = (chi (X,X)) . s ) by A1, PARTFUN1:3;
hence contradiction by A2, FUNCT_3:def 3; :: thesis: verum

end;

hence 0 < r by A1; :: thesis: verum

end;

hence chi (X,X) is positive-yielding by PARTFUN3:def 1; :: thesis: verum