let a, b, c, x, y, z be object ; :: thesis: ( ( 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 :: thesis: ((a,b,c) --> (x,y,z)) . c = z

assume b <> c ; :: thesis: ((a,b,c) --> (x,y,z)) . b = y
then 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 ; :: thesis: verum

end;

thus ((a,b,c) --> (x,y,z)) . c = (c .--> z) . c by A1, A2, Th13
.= z by FUNCOP_1:72 ; :: thesis: verum