let G be Group; :: thesis: for G1 being Subgroup of G
for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds
[.G1,((Omega). G).] is Subgroup of N
let G1 be Subgroup of G; :: thesis: for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds
[.G1,((Omega). G).] is Subgroup of N
let N be strict normal Subgroup of G; :: thesis: ( N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) implies [.G1,((Omega). G).] is Subgroup of N )
assume that
A1: N is Subgroup of G1 and
A2: G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) ; :: thesis: [.G1,((Omega). G).] is Subgroup of N
A3: (G1,N) `*` = N by A1, GROUP_6:def 1;
reconsider J = G1 ./. ((G1,N) `*`) as Subgroup of G ./. N by A1, GROUP_6:28;
reconsider I = N as normal Subgroup of G1 by A3;
A4: commutators (G1,((Omega). G)) c= carr N

proof

now :: thesis: for x being Element of G st x in commutators (G1,((Omega). G)) holds
x in carr N

let x be Element of G; :: thesis: ( x in commutators (G1,((Omega). G)) implies x in carr N )
assume x in commutators (G1,((Omega). G)) ; :: thesis: x in carr N
then consider a, b being Element of G such that
A5: ( x = [.a,b.] & a in G1 & b in (Omega). G ) by GROUP_5:52;
reconsider c = a as Element of G1 by A5, STRUCT_0:def 5;
reconsider S9 = c * I as Element of J by A3, GROUP_6:22;
A6: S9 in J by STRUCT_0:def 5;
reconsider T = b * N as Element of (G ./. N) by GROUP_6:14;
reconsider d = c as Element of G ;
d * N = c * I by GROUP_6:2;
then reconsider S = S9 as Element of (G ./. N) by GROUP_6:14;
S in center (G ./. N) by A2, A6, GROUP_2:40;
then A7: S * T = T * S by GROUP_5:77;
A8: ( S = d * N & T = b * N & @ S = S & @ T = T ) by GROUP_6:2;
then A9: S * T = (d * N) * (b * N) by GROUP_6:def 3
.= d * (N * (b * N)) by GROUP_3:10
.= d * ((N * b) * N) by GROUP_3:13
.= d * ((b * N) * N) by GROUP_3:117
.= d * (b * N) by GROUP_6:5
.= (d * b) * N by GROUP_2:105 ;
T * S = (b * N) * (d * N) by A8, GROUP_6:def 3
.= b * (N * (d * N)) by GROUP_3:10
.= b * ((N * d) * N) by GROUP_3:13
.= b * ((d * N) * N) by GROUP_3:117
.= b * (d * N) by GROUP_6:5
.= (b * d) * N by GROUP_2:105 ;
then A10: ((d ") * (b ")) * ((d * b) * N) = (((d ") * (b ")) * (b * d)) * N by A7, A9, GROUP_2:105
.= ((d ") * ((b ") * (b * d))) * N by GROUP_1:def 3
.= ((d ") * (((b ") * b) * d)) * N by GROUP_1:def 3
.= ((d ") * ((1_ G) * d)) * N by GROUP_1:def 5
.= ((d ") * d) * N by GROUP_1:def 4
.= (1_ G) * N by GROUP_1:def 5
.= carr N by GROUP_2:109 ;
((d ") * (b ")) * ((d * b) * N) = (((d ") * (b ")) * (d * b)) * N by GROUP_2:105
.= [.d,b.] * N by GROUP_5:16 ;
then [.d,b.] in N by A10, GROUP_2:113;
hence x in carr N by A5, STRUCT_0:def 5; :: thesis: verum

end;

hence commutators (G1,((Omega). G)) c= carr N ; :: thesis: verum

end;

gr (carr N) = N by GROUP_4:31;
hence [.G1,((Omega). G).] is Subgroup of N by A4, GROUP_4:32; :: thesis: verum