A1: dom f = X by FUNCT_2:def 1;
a in REAL by XREAL_0:def 1;
then (dom f) --> a is Function of X,REAL by A1, FUNCOP_1:45;
then reconsider g = <:((dom f) --> a),f:> as Function of X,[:REAL,Y:] by FUNCT_3:58;
F [;] (a,f) = F * g by FUNCOP_1:def 5;
hence F [;] (a,f) is Element of Funcs (X,Y) by FUNCT_2:8; :: thesis: verum