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

x in ExtREAL

then
( dom (chi (A,X)) = X & rng (chi (A,X)) c= ExtREAL )
by FUNCT_3:def 3;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

hence x in ExtREAL ; :: thesis: verum

end;assume A1: x in rng (chi (A,X)) ; :: thesis: x in ExtREAL

hence x in ExtREAL ; :: thesis: verum

hence chi (A,X) is PartFunc of X,ExtREAL by RELSET_1:4; :: thesis: verum