set F = sqrt f;
A1: dom (sqrt f) = dom f by Def5;
rng (sqrt f) c= REAL by VALUED_0:def 3;
then sqrt f is PartFunc of (dom (sqrt f)),REAL by RELSET_1:11;
hence sqrt f is PartFunc of C,REAL by A1, RELSET_1:13; :: thesis: verum