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