theorem Th111: :: GROUP_1A:157

for G being addGroup
for a being Element of G holds
( a + ((Omega). G) = the carrier of G & ((Omega). G) + a = the carrier of G )