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