now :: thesis: for x being object holds (~ f) . x < +infty

let x be object ; :: thesis: (~ f) . b₁ < +infty

per cases ( x in dom (~ f) or not x in dom (~ f) ) ;

suppose x in dom (~ f) ; :: thesis: (~ f) . b₁ < +infty

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) < +infty by MESFUNC5:def 6;
then (~ f) . (b,a) < +infty by FUNCT_4:def 8;
hence (~ f) . x < +infty by A1; :: thesis: verum

end;

suppose not x in dom (~ f) ; :: thesis: (~ f) . b₁ < +infty

hence (~ f) . x < +infty by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence ~ f is without+infty by MESFUNC5:def 6; :: thesis: verum