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) )
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 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;
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) ; :: 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