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

.= 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