let C1 be non empty set ; 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; 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; verum