f .: g1,g2 = f * <:g1,g2:> by FUNCOP_1:def 3;
then ( dom (f .: g1,g2) = A & rng (f .: g1,g2) c= D ) by FUNCT_2:def 1, RELAT_1:def 19;
hence f .: g1,g2 is Element of Funcs A,D by FUNCT_2:def 2; :: thesis: verum