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

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

now :: thesis: for b being Element of G st b in [.N1,N2.] |^ a holds
b in [.N1,N2.]

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:58;
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:28;
A6: len (F |^ a) = len F by Def1;
A7: rng (F |^ a) c= commutators ((carr N1),(carr N2))

proof

let x be object ; :: 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 object such that
A8: y in dom (F |^ a) and
A9: (F |^ a) . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A8;
A10: y in dom F by A6, A8, FINSEQ_3:29;
then A11: F . y = F /. y by PARTFUN1:def 6;
y in dom F by A6, A8, FINSEQ_3:29;
then F . y in rng F by FUNCT_1:def 3;
then consider d, e being Element of G such that
A12: F . y = [.d,e.] and
A13: d in carr N1 and
A14: e in carr N2 by A4, Th47;
d in N1 by A13, STRUCT_0:def 5;
then d |^ a in N1 |^ a by GROUP_3:58;
then d |^ a in N1 by GROUP_3:def 13;
then A15: d |^ a in carr N1 by STRUCT_0:def 5;
e in N2 by A14, STRUCT_0:def 5;
then e |^ a in N2 |^ a by GROUP_3:58;
then e |^ a in N2 by GROUP_3:def 13;
then A16: e |^ a in carr N2 by STRUCT_0:def 5;
x = (F /. y) |^ a by A9, A10, Def1;
then x = [.(d |^ a),(e |^ a).] by A12, A11, Th23;
hence x in commutators ((carr N1),(carr N2)) by A15, A16; :: thesis: verum

end;

b = Product ((F |^ I) |^ a) by A1, A5, Th14
.= Product ((F |^ a) |^ I) by Th15 ;
hence b in [.N1,N2.] by A3, A6, A7, GROUP_4:28; :: thesis: verum

end;

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

end;

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