:: deftheorem defines nonnegative-yielding DBLSEQ_2:def 1 :
for f being Function of [:NAT,NAT:],REAL holds
( f is nonnegative-yielding iff for i, j being Nat holds f . (i,j) >= 0 );