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

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