let a, b, c, x, y, z be object ; ( ( b <> c implies ((a,b,c) --> (x,y,z)) . b = y ) & ((a,b,c) --> (x,y,z)) . c = z )
set f = (a,b) --> (x,y);
set g = c .--> z;
set h = (a,b,c) --> (x,y,z);
A1:
c in {c}
by TARSKI:def 1;
A2:
dom (c .--> z) = {c}
;
hereby ((a,b,c) --> (x,y,z)) . c = z
assume
b <> c
;
((a,b,c) --> (x,y,z)) . b = ythen A3:
not
b in {c}
by TARSKI:def 1;
thus ((a,b,c) --> (x,y,z)) . b =
((a,b) --> (x,y)) . b
by A3, A2, Th11
.=
y
by Th63
;
verum
end;
thus ((a,b,c) --> (x,y,z)) . c =
(c .--> z) . c
by A1, A2, Th13
.=
z
by FUNCOP_1:72
; verum