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