A1: 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

A3: now

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

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

thus x in ExtREAL by A4; :: thesis: verum

end;

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

thus x in ExtREAL by A5; :: thesis: verum

end;

end;

end;

thus x in ExtREAL by A3; :: thesis: verum

end;

A6: ( dom (chi A,X) = X & rng (chi A,X) c= ExtREAL ) by A1, FUNCT_3:def 3, TARSKI:def 3;
thus chi A,X is PartFunc of X,ExtREAL by A6, RELSET_1:11; :: thesis: verum