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