let f be FinSequence; :: thesis: ( f is nonnegative-yielding & f is INT -valued implies f is NAT -valued )
assume A1: ( f is nonnegative-yielding & f is INT -valued ) ; :: thesis: f is NAT -valued
then reconsider f = f as FinSequence of INT by NEWTON02:103;
reconsider f = f as FinSequence of REAL by FINSEQ_2:24, NUMBERS:15;
for i being Nat st i in dom f holds
f . i in NAT by A1, INT_1:3;
hence f is NAT -valued by FINSEQ_2:12; :: thesis: verum