dom (chi X,C) = C by FUNCT_3:def 3;
hence for b₁ being PartFunc of C,REAL st b₁ = chi X,C holds
b₁ is total by PARTFUN1:def 4; :: thesis: verum