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

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