theorem :: GROUP_1A:91
for G being addGroup
for H1, H2 being Subgroup of G holds 0_ H1 = 0_ H2