let G be Group; :: thesis: for H being Subgroup of G
for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )
let H be Subgroup of G; :: thesis: for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )
let N be strict normal Subgroup of G; :: thesis: ( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )

now :: thesis: for a being Element of G st a in [.N,H.] holds
a in N

let a be Element of G; :: thesis: ( a in [.N,H.] implies a in N )
assume a in [.N,H.] ; :: thesis: a in N
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A1: len F = len I and
A2: rng F c= commutators (N,H) and
A3: a = Product (F |^ I) by Th61;
commutators (N,H) c= carr N by Th55;
then rng F c= carr N by A2;
then a in gr (carr N) by A1, A3, GROUP_4:28;
hence a in N by GROUP_4:31; :: thesis: verum

end;

hence [.N,H.] is Subgroup of N by GROUP_2:58; :: thesis: [.H,N.] is Subgroup of N

now :: thesis: for a being Element of G st a in [.H,N.] holds
a in N

let a be Element of G; :: thesis: ( a in [.H,N.] implies a in N )
assume a in [.H,N.] ; :: thesis: a in N
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A4: len F = len I and
A5: rng F c= commutators (H,N) and
A6: a = Product (F |^ I) by Th61;
commutators (H,N) c= carr N by Th55;
then rng F c= carr N by A5;
then a in gr (carr N) by A4, A6, GROUP_4:28;
hence a in N by GROUP_4:31; :: thesis: verum

end;

hence [.H,N.] is Subgroup of N by GROUP_2:58; :: thesis: verum