( dom |.f.| = dom f & rng |.f.| c= REAL ) by Def11, VALUED_0:def 3;
hence |.f.| is PartFunc of C,REAL by RELSET_1:4; :: thesis: verum