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