hereby :: thesis: ( ( for n being Element of NAT holds f . n >= 0 ) implies f is nonnegative )

assume A1: f is nonnegative ; :: thesis: for n being Element of NAT holds f . n >= 0
let n be Element of NAT ; :: thesis: f . n >= 0
f . n in rng f by VALUED_0:28;
hence f . n >= 0 by A1, PARTFUN3:def 4; :: thesis: verum

end;

assume A2: for n being Element of NAT holds f . n >= 0 ; :: thesis: f is nonnegative
let r be real number ; :: according to PARTFUN3:def 4 :: thesis: ( not r in K2(f) or 0 <= r )
assume r in rng f ; :: thesis: 0 <= r
then consider x being Element of NAT such that
A3: r = f . x by FUNCT_2:190;
thus 0 <= r by A2, A3; :: thesis: verum