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