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 N19 = multMagma(# the carrier of N1, the multF of N1 #), N29 = multMagma(# the carrier of N2, the multF of N2 #) as strict normal Subgroup of G by Lm6;
thus N1 * N2 = (carr N29) * (carr N19) by GROUP_3:125
.= N2 * N1 ; :: thesis: verum