F . n in Funcs (C,D) ;
hence F . n is Function of C,D by FUNCT_2:66; :: thesis: verum