let G be Group; :: thesis: for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
let N1, N2 be normal Subgroup of G; :: thesis: [.N1,N2.] is Subgroup of [.N2,N1.]

now

let a be Element of G; :: thesis: ( a in [.N1,N2.] implies a in [.N2,N1.] )
assume a in [.N1,N2.] ; :: thesis: a in [.N2,N1.]
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
len F = len I and
A1: rng F c= commutators N1,N2 and
A2: a = Product (F |^ I) by Th69;
deffunc H₁( Nat) -> Element of the carrier of G = (F /. $1) " ;
consider F1 being FinSequence of the carrier of G such that
A3: len F1 = len F and
A4: for k being Nat st k in dom F1 holds
F1 . k = H₁(k) from FINSEQ_2:sch 1();
A5: dom F1 = Seg (len F) by A3, FINSEQ_1:def 3;
deffunc H₂( Nat) -> Element of INT = @ (- (@ (I /. $1)));
consider I1 being FinSequence of INT such that
A6: len I1 = len F and
A7: for k being Nat st k in dom I1 holds
I1 . k = H₂(k) from FINSEQ_2:sch 1();
A9: dom F = Seg (len F) by FINSEQ_1:def 3;
A10: dom F1 = dom F by A3, FINSEQ_3:31;
A11: dom I1 = dom F by A6, FINSEQ_3:31;
set J = F1 |^ I1;
A12: ( len (F1 |^ I1) = len F & len (F |^ I) = len F ) by A3, GROUP_4:def 4;
then X: dom (F |^ I) = Seg (len F) by FINSEQ_1:def 3;

now

let k be Nat; :: thesis: ( k in dom (F |^ I) implies (F |^ I) . k = (F1 |^ I1) . k )
assume A13: k in dom (F |^ I) ; :: thesis: (F |^ I) . k = (F1 |^ I1) . k
then A14: k in dom F by X, FINSEQ_1:def 3;
( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k & F1 . k = (F /. k) " & I1 . k = I1 /. k & @ (I1 /. k) = I1 /. k & I1 . k = @ (- (@ (I /. k))) & @ (- (@ (I /. k))) = - (@ (I /. k)) ) by A4, A7, A9, A10, A11, A13, X, GROUP_4:def 4, PARTFUN1:def 8;
then (F1 |^ I1) . k = (((F /. k) " ) |^ (@ (I /. k))) " by GROUP_1:70
.= (((F /. k) |^ (@ (I /. k))) " ) " by GROUP_1:72
.= (F /. k) |^ (@ (I /. k)) ;
hence (F |^ I) . k = (F1 |^ I1) . k by A14, GROUP_4:def 4; :: thesis: verum

end;

then A15: F1 |^ I1 = F |^ I by A12, FINSEQ_2:10;
rng F1 c= commutators N2,N1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F1 or x in commutators N2,N1 )
assume x in rng F1 ; :: thesis: x in commutators N2,N1
then consider y being set such that
A16: y in dom F1 and
A17: F1 . y = x by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A16;
y in dom F by A3, A16, FINSEQ_3:31;
then F . y in rng F by FUNCT_1:def 5;
then consider b, c being Element of G such that
A18: F . y = [.b,c.] and
A19: ( b in N1 & c in N2 ) by A1, Th58;
y in dom F by A3, A16, FINSEQ_3:31;
then ( x = (F /. y) " & F /. y = F . y ) by A4, A9, A17, A5, PARTFUN1:def 8;
then x = [.c,b.] by A18, Th25;
hence x in commutators N2,N1 by A19, Th58; :: thesis: verum

end;

hence a in [.N2,N1.] by A2, A3, A6, A15, Th69; :: thesis: verum

end;

hence [.N1,N2.] is Subgroup of [.N2,N1.] by GROUP_2:67; :: thesis: verum