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 set 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 set 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 set 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 set 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 set 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 set ; :: 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:106;
hence f . x1,y1 = f . x2,y2 by A1, A2, FUNCT_1:def 16; :: thesis: verum

end;

assume A3: for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds
f . x1,y1 = f . x2,y2 ; :: thesis: f is constant
let x be set ; :: according to FUNCT_1:def 16 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or f . x = f . b₁ )
let y be set ; :: 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 set such that
A4: ( x1 in X & y1 in Y & x = [x1,y1] ) by A1, ZFMISC_1:103;
assume y in dom f ; :: thesis: f . x = f . y
then consider x2, y2 being set such that
A5: ( x2 in X & y2 in Y & y = [x2,y2] ) by A1, ZFMISC_1:103;
thus f . x = f . x1,y1 by A4
.= f . x2,y2 by A3, A4, A5
.= f . y by A5 ; :: thesis: verum