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