let G be Group; :: thesis: for H being Subgroup of G
for N being normal Subgroup of G holds [.N,H.] is Subgroup of N
let H be Subgroup of G; :: thesis: for N being normal Subgroup of G holds [.N,H.] is Subgroup of N
let N be normal Subgroup of G; :: thesis: [.N,H.] is Subgroup of N
( the carrier of N c= the carrier of G & the multF of N = the multF of G || the carrier of N ) by GROUP_2:def 5;
then reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict Subgroup of G by GROUP_2:def 5;

now :: thesis: for a being Element of G holds N9 |^ a = multMagma(# the carrier of N9, the multF of N9 #)

let a be Element of G; :: thesis: N9 |^ a = multMagma(# the carrier of N9, the multF of N9 #)
the carrier of (N |^ a) = (carr N) |^ a by GROUP_3:def 6
.= (carr N9) |^ a
.= the carrier of (N9 |^ a) by GROUP_3:def 6 ;
hence N9 |^ a = N |^ a by GROUP_2:59
.= multMagma(# the carrier of N9, the multF of N9 #) by GROUP_3:def 13 ;
:: thesis: verum

end;

then reconsider N9 = N9 as strict normal Subgroup of G by GROUP_3:def 13;
[.N9,H.] = [.N,H.] ;
then A1: [.N,H.] is Subgroup of N9 by GROUP_5:67;
N9 is Subgroup of N by GROUP_2:57;
hence [.N,H.] is Subgroup of N by A1, GROUP_2:56; :: thesis: verum