now :: thesis: for x being object st x in rng (chi (A,X)) holds
x in ExtREAL

let x be object ; :: thesis: ( x in rng (chi (A,X)) implies x in ExtREAL )
assume A1: x in rng (chi (A,X)) ; :: thesis: x in ExtREAL

now :: thesis: x in ExtREAL

per cases ( x = 0. or x = 1. ) by A1, TARSKI:def 2;

suppose x = 0. ; :: thesis: x in ExtREAL

hence x in ExtREAL ; :: thesis: verum

end;

suppose x = 1. ; :: thesis: x in ExtREAL

hence x in ExtREAL ; :: thesis: verum

end;

end;

end;

hence x in ExtREAL ; :: thesis: verum

end;

then ( dom (chi (A,X)) = X & rng (chi (A,X)) c= ExtREAL ) by FUNCT_3:def 3;
hence chi (A,X) is PartFunc of X,ExtREAL by RELSET_1:4; :: thesis: verum