theorem Th61: :: GROUP_1A:262

for G being addGroup
for H being strict Subgroup of G holds H * (0_ G) = H