let C1 be non empty set ; :: thesis: for f being RMembership_Func of C1,C1 holds f (#) (Zmf C1,C1) = (Zmf C1,C1) (#) f
let f be RMembership_Func of C1,C1; :: thesis: f (#) (Zmf C1,C1) = (Zmf C1,C1) (#) f
f (#) (Zmf C1,C1) = Zmf C1,C1 by Th23;
hence f (#) (Zmf C1,C1) = (Zmf C1,C1) (#) f by Th22; :: thesis: verum