now

let x be set ; :: thesis: ( x in rng (chi (X,C)) implies x in REAL )
assume x in rng (chi (X,C)) ; :: thesis: x in REAL
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence x in REAL ; :: thesis: verum

end;

then A1: rng (chi (X,C)) c= REAL by TARSKI:def 3;
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