let a, b, c be object ; :: thesis: (a,a) --> (b,c) = a .--> c
dom (a .--> c) = {a}
.= dom ({a} --> b) ;
hence (a,a) --> (b,c) = a .--> c by Th19; :: thesis: verum