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