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