let G be Group; :: thesis: for A, B being Subgroup of G holds [.A,B.] is Subgroup of [.B,A.]
let A, B be Subgroup of G; :: thesis: [.A,B.] is Subgroup of [.B,A.]

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

let a be Element of G; :: thesis: ( a in [.A,B.] implies a in [.B,A.] )
assume a in [.A,B.] ; :: thesis: a in [.B,A.]
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 (A,B) and
A2: a = Product (F |^ I) by GROUP_5:61;
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();
A8: dom F = Seg (len F) by FINSEQ_1:def 3;
A9: dom F1 = dom F by A3, FINSEQ_3:29;
A10: dom I1 = dom F by A6, FINSEQ_3:29;
set J = F1 |^ I1;
A11: ( len (F1 |^ I1) = len F & len (F |^ I) = len F ) by A3, GROUP_4:def 3;
then A12: dom (F |^ I) = Seg (len F) by FINSEQ_1:def 3;

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 A13: k in dom (F |^ I) ; :: thesis: (F |^ I) . k = (F1 |^ I1) . k
then A14: k in dom F by A12, 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, A8, A9, A10, A13, A12, GROUP_4:def 3, PARTFUN1:def 6;
then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by GROUP_1:36
.= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37
.= (F /. k) |^ (@ (I /. k)) ;
hence (F |^ I) . k = (F1 |^ I1) . k by A14, GROUP_4:def 3; :: thesis: verum

end;

then A15: F1 |^ I1 = F |^ I by A11, FINSEQ_2:9;
rng F1 c= commutators (B,A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F1 or x in commutators (B,A) )
assume x in rng F1 ; :: thesis: x in commutators (B,A)
then consider y being object such that
A16: y in dom F1 and
A17: F1 . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A16;
y in dom F by A3, A16, FINSEQ_3:29;
then F . y in rng F by FUNCT_1:def 3;
then consider b, c being Element of G such that
A18: F . y = [.b,c.] and
A19: ( b in A & c in B ) by A1, GROUP_5:52;
( x = (F /. y) " & F /. y = F . y ) by A16, A4, A8, A17, A5, PARTFUN1:def 6;
then x = [.c,b.] by A18, GROUP_5:22;
hence x in commutators (B,A) by A19, GROUP_5:52; :: thesis: verum

end;

hence a in [.B,A.] by A2, A3, A6, A15, GROUP_5:61; :: thesis: verum

end;

hence [.A,B.] is Subgroup of [.B,A.] by GROUP_2:58; :: thesis: verum