dom |.f.| = dom f by Def11
.= C by FUNCT_2:def 1 ;
hence for b₁ being PartFunc of C,REAL st b₁ = |.f.| holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum