set f = the finite-support Function of X,NAT;
reconsider f = the finite-support Function of X,NAT as Function of X,COMPLEX by NUMBERS:20, FUNCT_2:7;
take f ; :: thesis: ( f is nonnegative-yielding & f is finite-support )
for r being Real st r in rng f holds
r >= 0 ;
then f is nonnegative-yielding by PARTFUN3:def 4;
hence ( f is nonnegative-yielding & f is finite-support ) ; :: thesis: verum