( {{} ,1} <> {} & dom (chi A,X) = X & rng (chi A,X) c= {{} ,1} ) by Def3, Th48;
hence chi A,X is Function of X,{{} ,1} by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum