dom (SC --> d) = SC by FUNCOP_1:19;
hence SC --> d is PartFunc of C,D by RELSET_1:17; :: thesis: verum