let G be Group; :: thesis: for a being Element of G holds
( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )
let a be Element of G; :: thesis: ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )
([#] the carrier of G) * a = the carrier of G by Th21;
hence ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) by Th21; :: thesis: verum