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 2; :: thesis: verum