dom |.f.| = dom f by Def11
.= C by FUNCT_2:def 1 ;
hence |.f.| is total PartFunc of C, REAL by PARTFUN1:def 4; :: thesis: verum