dom g = A by FUNCT_2:def 1;
then f [;] (d,g) = f * <:(A --> d),g:> by FUNCOP_1:def 5;
then ( dom (f [;] (d,g)) = A & rng (f [;] (d,g)) c= D ) by FUNCT_2:def 1, RELAT_1:def 19;
hence f [;] (d,g) is Element of Funcs (A,D) by FUNCT_2:def 2; :: thesis: verum