A1: dom (f *') = dom f by Def1
.= C by PARTFUN1:def 2 ;
for x being object st x in C holds
(f *') . x in COMPLEX by XCMPLX_0:def 2;
hence f *' is Function of C,COMPLEX by A1, FUNCT_2:3; :: thesis: verum