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