let a, b, x, y, x9, y9 be set ; :: thesis: ( 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) ; :: thesis: ( x = x9 & y = y9 )
thus x = ((a,b) --> (x,y)) . a by A1, FUNCT_4:63
.= x9 by A1, A2, FUNCT_4:63 ; :: thesis: y = y9
thus y = ((a,b) --> (x,y)) . b by FUNCT_4:63
.= y9 by A2, FUNCT_4:63 ; :: thesis: verum