thus
( f is nonnegative-yielding implies for i, j being Nat holds f . (i,j) >= 0 )
( ( for i, j being Nat holds f . (i,j) >= 0 ) implies f is nonnegative-yielding )
assume A1:
for i, j being Nat holds f . (i,j) >= 0
; f is nonnegative-yielding
let r be Real; PARTFUN3:def 4 ( not r in proj2 f or 0 <= r )
assume
r in rng f
; 0 <= r
then consider x being Element of [:NAT,NAT:] such that
A2:
r = f . x
by FUNCT_2:113;
consider x1, x2 being object such that
A3:
( x1 in NAT & x2 in NAT & x = [x1,x2] )
by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Nat by A3;
r = f . (x1,x2)
by A3, A2;
hence
0 <= r
by A1; verum