let G be Group; :: thesis: for H being Subgroup of G
for N being normal Subgroup of G holds H * N = N * H
let H be Subgroup of G; :: thesis: for N being normal Subgroup of G holds H * N = N * H
let N be normal Subgroup of G; :: thesis: H * N = N * H
thus H * N = (carr H) * N
.= N * (carr H) by GROUP_3:120
.= N * H ; :: thesis: verum