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:57;
then reconsider g = <:((dom f) --> a),f:> as Function of X,[:REAL ,Y:] by FUNCT_3:78;
F [;] a,f = F * g by FUNCOP_1:def 5;
hence F [;] a,f is Element of Funcs X,Y by FUNCT_2:11; :: thesis: verum