A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f = f as Function of V,COMPLEX ;
f *' is Function of V,COMPLEX ;
hence f *' is Functional of V by A1; :: thesis: verum