let a, b, c, d, x, y, z, w, x9, y9, z9, w9 be object ; ( 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)
; ( 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; verum