let a, b, c be set ; :: thesis: (a,a) --> (b,c) = a .--> c
dom (a .--> c) = {a} by FUNCOP_1:13
.= dom ({a} --> b) by FUNCOP_1:13 ;
hence (a,a) --> (b,c) = a .--> c by Th20; :: thesis: verum