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

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