dom (chi (A,X)) = X by FUNCT_3:def 3;
hence chi (A,X) is Function of X,ExtREAL by FUNCT_2:def 1; :: thesis: verum