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 ((Omega). G) = carr ((Omega). G) & (Omega). G = multMagma(# the carrier of G,the multF of G #) & [#] the carrier of G = the carrier of G & ([#] the carrier of G) * a = the carrier of G & a * ([#] the carrier of G) = the carrier of G & a * ((Omega). G) = a * (carr ((Omega). G)) & (carr ((Omega). G)) * a = ((Omega). G) * a ) by Th21;
hence ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) ; :: thesis: verum