( 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:4; :: thesis: verum