set f = the finite-support Function of X,NAT;

reconsider f = the finite-support Function of X,NAT as Function of X,REAL by NUMBERS:19, FUNCT_2:7;

take f ; :: thesis: ( f is finite-support & f is nonnegative-yielding )

for r being Real st r in rng f holds

r >= 0 ;

then f is nonnegative-yielding by PARTFUN3:def 4;

hence ( f is finite-support & f is nonnegative-yielding ) ; :: thesis: verum

reconsider f = the finite-support Function of X,NAT as Function of X,REAL by NUMBERS:19, FUNCT_2:7;

take f ; :: thesis: ( f is finite-support & f is nonnegative-yielding )

for r being Real st r in rng f holds

r >= 0 ;

then f is nonnegative-yielding by PARTFUN3:def 4;

hence ( f is finite-support & f is nonnegative-yielding ) ; :: thesis: verum