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