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