( dom (id SD) = SD & rng (id SD) = SD ) by RELAT_1:71;
hence id SD is PartFunc of D,D by RELSET_1:11; :: thesis: verum