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

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