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

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