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