let O be set ; :: thesis: for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 * N2 = N2 * N1
let G be GroupWithOperators of O; :: thesis: for N1, N2 being strict normal StableSubgroup of G holds N1 * N2 = N2 * N1
let N1, N2 be strict normal StableSubgroup of G; :: thesis: N1 * N2 = N2 * N1
reconsider N1' = multMagma(# the carrier of N1,the multF of N1 #), N2' = multMagma(# the carrier of N2,the multF of N2 #) as strict normal Subgroup of G by Lm7;
thus N1 * N2 = (carr N2') * (carr N1') by GROUP_3:148
.= N2 * N1 ; :: thesis: verum