let a, b, x, y, x', y' be set ; :: thesis: ( a <> b & a,b --> x,y = a,b --> x',y' implies ( x = x' & y = y' ) )
assume that
A1: a <> b and
A2: a,b --> x,y = a,b --> x',y' ; :: thesis: ( x = x' & y = y' )
thus x = (a,b --> x,y) . a by A1, Th66
.= x' by A1, A2, Th66 ; :: thesis: y = y'
thus y = (a,b --> x,y) . b by Th66
.= y' by A2, Th66 ; :: thesis: verum