let C be non empty set ; :: thesis: chi {} ,C is Membership_Func of C
A1: rng (chi {} ,C) c= [.0 ,1.] by Th1;
dom (chi {} ,C) = C by FUNCT_3:def 3;
hence chi {} ,C is Membership_Func of C by A1, Def1; :: thesis: verum