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 Lm7;
A1: H = (Omega). G9 ;
the carrier of (G ./. ((Omega). G)) = Cosets H by Def14
.= {the carrier of G} by A1, GROUP_2:172 ;
hence G ./. ((Omega). G) is trivial by GROUP_6:def 2; :: thesis: verum