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