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