theorem Th16: :: GROUP_1A:351

for H being non empty addMagma
for P being Subset of H
for h being Element of H holds (+ h) .: P = P + h