thus ( f is_less_than g iff for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) ) :: thesis: verum

proof

hereby :: thesis: ( ( for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) ) implies f is_less_than g )

assume A1: f is_less_than g ; :: thesis: for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y)
thus for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) :: thesis: verum

proof

let x be Element of X; :: thesis: for y being Element of Y holds f . (x,y) <= g . (x,y)
let y be Element of Y; :: thesis: f . (x,y) <= g . (x,y)
( dom f = [:X,Y:] & [x,y] in [:X,Y:] ) by FUNCT_2:def 1;
hence f . (x,y) <= g . (x,y) by A1; :: thesis: verum

end;

end;

assume A2: for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) ; :: thesis: f is_less_than g
A3: for c being set st c in dom f holds
f . c <= g . c

proof

let c be set ; :: thesis: ( c in dom f implies f . c <= g . c )
assume A4: c in dom f ; :: thesis: f . c <= g . c
then consider x, y being object such that
A5: [x,y] = c by RELAT_1:def 1;
reconsider y = y as Element of Y by A4, A5, ZFMISC_1:87;
reconsider x = x as Element of X by A4, A5, ZFMISC_1:87;
f . (x,y) <= g . (x,y) by A2;
hence f . c <= g . c by A5; :: thesis: verum

end;

dom g = [:X,Y:] by FUNCT_2:def 1;
hence f is_less_than g by A3; :: thesis: verum

end;