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