let a, b, c, d, x, y, z, w, x9, y9, z9, w9 be object ; :: thesis: ( a,b,c,d are_mutually_distinct & (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_distinct 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, Th142
.= x9 by A1, A2, Th142 ;
A4: y = ((a,b,c,d) --> (x,y,z,w)) . b by A1, Th141
.= y9 by A1, A2, Th141 ;
A5: z = ((a,b,c,d) --> (x,y,z,w)) . c by A1, Th140
.= z9 by A1, A2, Th140 ;
w = ((a,b,c,d) --> (x,y,z,w)) . d by Th139
.= w9 by A2, Th139 ;
hence ( x = x9 & y = y9 & z = z9 & w = w9 ) by A3, A4, A5; :: thesis: verum