now :: thesis: for x being object st x in dom (~ f) holds
(~ f) . x >= 0

let x be object ; :: thesis: ( x in dom (~ f) implies (~ f) . x >= 0 )
assume x in dom (~ f) ; :: thesis: (~ f) . x >= 0
then consider b, a being object such that
A1: ( b in B & a in A & x = [b,a] ) by ZFMISC_1:def 2;
reconsider a = a as Element of A by A1;
reconsider b = b as Element of B by A1;
f . (a,b) >= 0 by SUPINF_2:51;
then (~ f) . (b,a) >= 0 by FUNCT_4:def 8;
hence (~ f) . x >= 0 by A1; :: thesis: verum

end;

hence ~ f is nonnegative by SUPINF_2:52; :: thesis: verum