theorem :: GROUP_1A:171
for G being addGroup
for a being Element of G
for H1, H2 being Subgroup of G holds a + (H1 /\ H2) = (a + H1) /\ (a + H2)