theorem Th25: :: GROUP_1A:25

for G being addGroup
for h being Element of G holds 1 * h = h