dom (f " ) = dom f by Def7
.= C by FUNCT_2:def 1 ;
hence for b₁ being PartFunc of C,REAL st b₁ = f " holds
b₁ is total by PARTFUN1:def 4; :: thesis: verum