theorem Th69: :: GROUP_1A:270

for G being addGroup
for a being Element of G holds ((Omega). G) * a = (Omega). G