now

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

now

per cases ( x = 0. or x = 1. ) by A2, 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:11; :: thesis: verum