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