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

( 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