let G be addGroup; :: 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 ThX17;
hence ( a + ((Omega). G) = the carrier of G & ((Omega). G) + a = the carrier of G ) by ThX17; :: thesis: verum