for x being object st x in rng (chi (X,C)) holds
x in REAL by XREAL_0:def 1;
then A1: rng (chi (X,C)) c= REAL ;
dom (chi (X,C)) = C by FUNCT_3:def 3;
hence chi (X,C) is PartFunc of C,REAL by A1, RELSET_1:4; :: thesis: verum