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