theorem ThB52: :: GROUP_1A:253

for G being addGroup
for A being Subset of G holds A * (0_ G) = A