theorem :: GROUP_1A:324

for G being addGroup
for N1, N2 being strict normal Subgroup of G holds (carr N1) + (carr N2) = (carr N2) + (carr N1) by Lm5;