let a, b, x, y, x9, y9 be set ; ( a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) implies ( x = x9 & y = y9 ) )
assume that
A1:
a <> b
and
A2:
(a,b) --> (x,y) = (a,b) --> (x9,y9)
; ( x = x9 & y = y9 )
thus x =
((a,b) --> (x,y)) . a
by A1, FUNCT_4:63
.=
x9
by A1, A2, FUNCT_4:63
; y = y9
thus y =
((a,b) --> (x,y)) . b
by FUNCT_4:63
.=
y9
by A2, FUNCT_4:63
; verum