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

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

proof

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

hence f is_less_than g by A3; :: thesis: verum

end;

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 A2:
for x being Element of Xfor 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

end;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

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

dom g = [:X,Y:]
by FUNCT_2:def 1;
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;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

hence f is_less_than g by A3; :: thesis: verum