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