theorem ThA24: :: GROUP_1A:24

for G being addGroup
for h being Element of G holds 0 * h = 0_ G by Def7;