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

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