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 )

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

hence
[.N,H.] is Subgroup of N
by GROUP_2:58; :: thesis: [.H,N.] is Subgroup of Na 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;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

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

a in N

hence
[.H,N.] is Subgroup of N
by GROUP_2:58; :: thesis: veruma 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;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