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

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