let X, Y be set ; :: thesis: for f being Function st dom f = [:X,Y:] holds

( f is constant iff for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) )

let f be Function; :: thesis: ( dom f = [:X,Y:] implies ( f is constant iff for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) ) )

assume A1: dom f = [:X,Y:] ; :: thesis: ( f is constant iff for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) )

f . (x1,y1) = f . (x2,y2) ; :: thesis: f is constant

let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )

assume x in dom f ; :: thesis: ( not y in dom f or f . x = f . y )

then consider x1, y1 being object such that

A4: ( x1 in X & y1 in Y ) and

A5: x = [x1,y1] by A1, ZFMISC_1:84;

assume y in dom f ; :: thesis: f . x = f . y

then consider x2, y2 being object such that

A6: ( x2 in X & y2 in Y ) and

A7: y = [x2,y2] by A1, ZFMISC_1:84;

thus f . x = f . (x1,y1) by A5

.= f . (x2,y2) by A3, A4, A6

.= f . y by A7 ; :: thesis: verum

( f is constant iff for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) )

let f be Function; :: thesis: ( dom f = [:X,Y:] implies ( f is constant iff for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) ) )

assume A1: dom f = [:X,Y:] ; :: thesis: ( f is constant iff for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) )

hereby :: thesis: ( ( for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) ) implies f is constant )

assume A3:
for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds f . (x1,y1) = f . (x2,y2) ) implies f is constant )

assume A2:
f is constant
; :: thesis: for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2)

let x1, x2, y1, y2 be object ; :: thesis: ( x1 in X & x2 in X & y1 in Y & y2 in Y implies f . (x1,y1) = f . (x2,y2) )

assume ( x1 in X & x2 in X & y1 in Y & y2 in Y ) ; :: thesis: f . (x1,y1) = f . (x2,y2)

then ( [x1,y1] in [:X,Y:] & [x2,y2] in [:X,Y:] ) by ZFMISC_1:87;

hence f . (x1,y1) = f . (x2,y2) by A1, A2; :: thesis: verum

end;f . (x1,y1) = f . (x2,y2)

let x1, x2, y1, y2 be object ; :: thesis: ( x1 in X & x2 in X & y1 in Y & y2 in Y implies f . (x1,y1) = f . (x2,y2) )

assume ( x1 in X & x2 in X & y1 in Y & y2 in Y ) ; :: thesis: f . (x1,y1) = f . (x2,y2)

then ( [x1,y1] in [:X,Y:] & [x2,y2] in [:X,Y:] ) by ZFMISC_1:87;

hence f . (x1,y1) = f . (x2,y2) by A1, A2; :: thesis: verum

f . (x1,y1) = f . (x2,y2) ; :: thesis: f is constant

let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )

assume x in dom f ; :: thesis: ( not y in dom f or f . x = f . y )

then consider x1, y1 being object such that

A4: ( x1 in X & y1 in Y ) and

A5: x = [x1,y1] by A1, ZFMISC_1:84;

assume y in dom f ; :: thesis: f . x = f . y

then consider x2, y2 being object such that

A6: ( x2 in X & y2 in Y ) and

A7: y = [x2,y2] by A1, ZFMISC_1:84;

thus f . x = f . (x1,y1) by A5

.= f . (x2,y2) by A3, A4, A6

.= f . y by A7 ; :: thesis: verum