theorem :: GROUP_1A:27

for G being addGroup
for h being Element of G holds 3 * h = (h + h) + h