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