theorem Th125: :: GROUP_3:125

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