let G be Group; :: thesis: G ./. ((Omega). G) is trivial
the carrier of (G ./. ((Omega). G)) = { the carrier of G} by GROUP_2:142;
hence G ./. ((Omega). G) is trivial by Def2; :: thesis: verum