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

now

let a be Element of G; :: thesis: [.N1,N2.] |^ a is Subgroup of [.N1,N2.]

now

let b be Element of G; :: thesis: ( b in [.N1,N2.] |^ a implies b in [.N1,N2.] )
assume b in [.N1,N2.] |^ a ; :: thesis: b in [.N1,N2.]
then consider c being Element of G such that
A1: b = c |^ a and
A2: c in [.N1,N2.] by GROUP_3:70;
consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A3: len F = len I and
A4: rng F c= commutators (carr N1),(carr N2) and
A5: c = Product (F |^ I) by A2, GROUP_4:37;
A6: b = Product ((F |^ I) |^ a) by A1, A5, Th17
.= Product ((F |^ a) |^ I) by Th18 ;
A7: len (F |^ a) = len F by Def1;
rng (F |^ a) c= commutators (carr N1),(carr N2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (F |^ a) or x in commutators (carr N1),(carr N2) )
assume x in rng (F |^ a) ; :: thesis: x in commutators (carr N1),(carr N2)
then consider y being set such that
A8: y in dom (F |^ a) and
A9: (F |^ a) . y = x by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A8;
y in dom F by A7, A8, FINSEQ_3:31;
then F . y in rng F by FUNCT_1:def 5;
then consider d, e being Element of G such that
A10: F . y = [.d,e.] and
A11: ( d in carr N1 & e in carr N2 ) by A4, Th52;
y in dom F by A7, A8, FINSEQ_3:31;
then ( x = (F /. y) |^ a & F . y = F /. y ) by A9, Def1, PARTFUN1:def 8;
then A12: x = [.(d |^ a),(e |^ a).] by A10, Th26;
( d in N1 & e in N2 ) by A11, STRUCT_0:def 5;
then ( d |^ a in N1 |^ a & e |^ a in N2 |^ a ) by GROUP_3:70;
then ( d |^ a in N1 & e |^ a in N2 ) by GROUP_3:def 13;
then ( d |^ a in carr N1 & e |^ a in carr N2 ) by STRUCT_0:def 5;
hence x in commutators (carr N1),(carr N2) by A12; :: thesis: verum

end;

hence b in [.N1,N2.] by A3, A6, A7, GROUP_4:37; :: thesis: verum

end;

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

end;

hence [.N1,N2.] is normal Subgroup of G by GROUP_3:145; :: thesis: verum