now :: thesis:

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

now :: thesis:

per cases by A1, TARSKI:def 2;

suppose x = 0. ; :: thesis:

hence x in ExtREAL ; :: thesis:

end;

suppose x = 1. ; :: thesis:

hence x in ExtREAL ; :: thesis:

end;

end;

end;

hence x in ExtREAL ; :: thesis:

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: