let O be set ; :: thesis: for G being strict GroupWithOperators of O holds G ./. ((Omega). G) is trivial
let G be strict GroupWithOperators of O; :: thesis: G ./. ((Omega). G) is trivial
reconsider G9 = G as Group ;
reconsider H = multMagma(# the carrier of ((Omega). G), the multF of ((Omega). G) #) as strict normal Subgroup of G by Lm6;
A1: H = (Omega). G9 ;
the carrier of (G ./. ((Omega). G)) = Cosets H by Def14
.= { the carrier of G} by A1, GROUP_2:142 ;
hence G ./. ((Omega). G) is trivial ; :: thesis: verum