A1: dom (chi X,C) = C by FUNCT_3:def 3;

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 rng (chi X,C) c= REAL by TARSKI:def 3;
hence chi X,C is PartFunc of C,REAL by A1, RELSET_1:11; :: thesis: verum