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