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