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