let a, b, c, x, y, z be object ; ( a <> b & a <> c implies ((a,b,c) --> (x,y,z)) . a = x )
assume that
A1:
a <> b
and
A2:
a <> c
; ((a,b,c) --> (x,y,z)) . a = x
not a in dom (c .--> z)
by A2, TARSKI:def 1;
hence ((a,b,c) --> (x,y,z)) . a =
((a,b) --> (x,y)) . a
by Th11
.=
x
by A1, Th63
;
verum