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