thus ( f is nonnegative implies for n being Nat holds f . n >= 0 ) by VALUED_0:28; :: thesis: ( ( for n being Nat holds f . n >= 0 ) implies f is nonnegative )
assume A1: for n being Nat holds f . n >= 0 ; :: thesis: f is nonnegative
let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( not r in rng f or 0 <= r )
assume r in rng f ; :: thesis: 0 <= r
then ex x being Element of NAT st r = f . x by FUNCT_2:113;
hence 0 <= r by A1; :: thesis: verum