let a, b, x, y, x9, y9 be object ; ( 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, Th63
.=
x9
by A1, A2, Th63
; y = y9
thus y =
((a,b) --> (x,y)) . b
by Th63
.=
y9
by A2, Th63
; verum