set F = f ^ ;
A1: rng (f ^ ) c= COMPLEX by VALUED_0:def 1;
dom (f ^ ) = (dom f) \ (f " {0 }) by Def8;
hence f ^ is PartFunc of C,COMPLEX by A1, RELSET_1:11; :: thesis: verum