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