( dom (f ^2) = dom f & rng (f ^2) c= COMPLEX ) by Th11;
hence f ^2 is PartFunc of C,COMPLEX by RELSET_1:4; :: thesis: verum