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