thus ( f is nonnegative-yielding implies for i, j being Nat holds f . (i,j) >= 0 ) :: thesis: ( ( for i, j being Nat holds f . (i,j) >= 0 ) implies f is nonnegative-yielding )

proof

assume A0: f is nonnegative-yielding ; :: thesis: for i, j being Nat holds f . (i,j) >= 0
let i, j be Nat; :: thesis: f . (i,j) >= 0
( i in NAT & j in NAT ) by ORDINAL1:def 12;
then [i,j] in [:NAT,NAT:] by ZFMISC_1:def 2;
hence f . (i,j) >= 0 by A0, FUNCT_2:4; :: thesis: verum

end;

assume A1: for i, j being Nat holds f . (i,j) >= 0 ; :: thesis: f is nonnegative-yielding
let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( not r in proj2 f or 0 <= r )
assume r in rng f ; :: thesis: 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; :: thesis: verum