theorem :: GROUP_1A:254

for G being addGroup
for A being Subset of G st A <> {} holds
(0_ G) * A = {(0_ G)}