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