let a, b, c, d, x, y, z, w, x9, y9, z9, w9 be set ; :: thesis: ( a,b,c,d are_mutually_different & (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) implies ( x = x9 & y = y9 & z = z9 & w = w9 ) )
assume that
A1: a,b,c,d are_mutually_different and
A2: (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) ; :: thesis: ( x = x9 & y = y9 & z = z9 & w = w9 )
A3: x = ((a,b,c,d) --> (x,y,z,w)) . a by A1, Th3
.= x9 by A1, A2, Th3 ;
A4: y = ((a,b,c,d) --> (x,y,z,w)) . b by A1, Th3
.= y9 by A1, A2, Th3 ;
A5: z = ((a,b,c,d) --> (x,y,z,w)) . c by A1, Th3
.= z9 by A1, A2, Th3 ;
w = ((a,b,c,d) --> (x,y,z,w)) . d by A1, Th3
.= w9 by A1, A2, Th3 ;
hence ( x = x9 & y = y9 & z = z9 & w = w9 ) by A3, A4, A5; :: thesis: verum