A1: dom f = the carrier of M by FUNCT_2:def 1;
reconsider g = <:((dom f) --> a),f:> as Function of M,[: the carrier of R, the carrier of N:] by A1, FUNCT_3:58;
F [;] (a,f) = F * g ;
hence F [;] (a,f) is Element of Funcs ( the carrier of M, the carrier of N) ; :: thesis: verum