let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1)
let N1, N2 be strict normal Subgroup of G; :: thesis: (carr N1) * (carr N2) = (carr N2) * (carr N1)
( (carr N1) * (carr N2) c= (carr N2) * (carr N1) & (carr N2) * (carr N1) c= (carr N1) * (carr N2) ) by Lm5;
hence (carr N1) * (carr N2) = (carr N2) * (carr N1) by XBOOLE_0:def 10; :: thesis: verum