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 :: thesis: for a being Element of G st a in [.N1,N2.] holds
a in [.N2,N1.]

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 Th61;
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 F = Seg (len F) by FINSEQ_1:def 3;
A6: rng F1 c= commutators (N2,N1)

proof

let x be object ; :: 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 object such that
A7: y in dom F1 and
A8: F1 . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A7;
y in dom F by A3, A7, FINSEQ_3:29;
then A9: F /. y = F . y by PARTFUN1:def 6;
y in dom F by A3, A7, FINSEQ_3:29;
then F . y in rng F by FUNCT_1:def 3;
then consider b, c being Element of G such that
A10: F . y = [.b,c.] and
A11: ( b in N1 & c in N2 ) by A1, Th52;
x = (F /. y) " by A4, A7, A8;
then x = [.c,b.] by A10, A9, Th22;
hence x in commutators (N2,N1) by A11, Th52; :: thesis: verum

end;

A12: len (F |^ I) = len F by GROUP_4:def 3;
then A13: dom (F |^ I) = Seg (len F) by FINSEQ_1:def 3;
deffunc H₂( Nat) -> Element of INT = @ (- (@ (I /. $1)));
consider I1 being FinSequence of INT such that
A14: len I1 = len F and
A15: for k being Nat st k in dom I1 holds
I1 . k = H₂(k) from FINSEQ_2:sch 1();
set J = F1 |^ I1;
A16: dom F1 = dom F by A3, FINSEQ_3:29;
A17: dom I1 = dom F by A14, FINSEQ_3:29;

A18: now :: thesis: for k being Nat st k in dom (F |^ I) holds
(F |^ I) . k = (F1 |^ I1) . k

let k be Nat; :: thesis: ( k in dom (F |^ I) implies (F |^ I) . k = (F1 |^ I1) . k )
assume A19: k in dom (F |^ I) ; :: thesis: (F |^ I) . k = (F1 |^ I1) . k
then A20: k in dom F by A13, FINSEQ_1:def 3;
A21: ( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k ) by A5, A16, A13, A19, GROUP_4:def 3, PARTFUN1:def 6;
A22: I1 . k = @ (- (@ (I /. k))) by A15, A5, A17, A13, A19;
( F1 . k = (F /. k) " & I1 . k = I1 /. k ) by A4, A5, A16, A17, A13, A19, PARTFUN1:def 6;
then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by A21, A22, GROUP_1:36
.= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37
.= (F /. k) |^ (@ (I /. k)) ;
hence (F |^ I) . k = (F1 |^ I1) . k by A20, GROUP_4:def 3; :: thesis: verum

end;

len (F1 |^ I1) = len F by A3, GROUP_4:def 3;
then F1 |^ I1 = F |^ I by A12, A18, FINSEQ_2:9;
hence a in [.N2,N1.] by A2, A3, A14, A6, Th61; :: thesis: verum

end;

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