now

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

now

per cases ( x = 0. or x = 1. ) by A1, MESFUNC1:def 8, 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, TARSKI:def 3;
hence chi (A,X) is PartFunc of X,ExtREAL by RELSET_1:4; :: thesis: verum