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

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