rng f c= D1 by RELAT_1:def 19;
then A2: rng f c= D2 by A1;
dom f = D by FUNCT_2:def 1;
hence f is Function of D,D2 by A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum