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 Th17;
hence ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) by Th17; :: thesis: verum