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