let G be Group; :: thesis: for G1 being Subgroup of G
for N being normal Subgroup of G st N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N holds
G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N)
let G1 be Subgroup of G; :: thesis: for N being normal Subgroup of G st N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N holds
G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N)
let N be normal Subgroup of G; :: thesis: ( N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N implies G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) )
assume that
A1: N is strict Subgroup of G1 and
A2: [.G1,((Omega). G).] is strict Subgroup of N ; :: thesis: G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. 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;
for S1 being Element of (G ./. N) st S1 in J holds
S1 in center (G ./. N)

proof

let S1 be Element of (G ./. N); :: thesis: ( S1 in J implies S1 in center (G ./. N) )
assume A4: S1 in J ; :: thesis: S1 in center (G ./. N)
for S being Element of (G ./. N) holds S1 * S = S * S1

proof

let S be Element of (G ./. N); :: thesis: S1 * S = S * S1
consider a being Element of G such that
A5: ( S = a * N & S = N * a ) by GROUP_6:21;
consider c being Element of G1 such that
A6: ( S1 = c * I & S1 = I * c ) by A3, A4, GROUP_6:23;
reconsider d = c as Element of G by GROUP_2:42;
A7: d in G1 by STRUCT_0:def 5;
a in (Omega). G by STRUCT_0:def 5;
then [.d,a.] in [.G1,((Omega). G).] by A7, GROUP_5:65;
then A8: [.d,a.] in N by A2, GROUP_2:40;
A9: ( @ S = S & @ S1 = S1 & c * I = d * N & N * d = I * c ) by GROUP_6:2;
then A10: S * S1 = (a * N) * (d * N) by A5, A6, GROUP_6:def 3
.= (a * d) * N by GROUP_11:1 ;
A11: S1 * S = (d * N) * (a * N) by A5, A6, A9, GROUP_6:def 3
.= (d * a) * N by GROUP_11:1 ;
A12: ((a * d) * [.d,a.]) * N = (a * d) * ([.d,a.] * N) by GROUP_2:32
.= (a * d) * N by A8, GROUP_2:113 ;
((a * d) * [.d,a.]) * N = ((a * d) * (((d ") * (a ")) * (d * a))) * N by GROUP_1:def 3
.= (((a * d) * ((d ") * (a "))) * (d * a)) * N by GROUP_1:def 3
.= ((a * (d * ((d ") * (a ")))) * (d * a)) * N by GROUP_1:def 3
.= ((a * ((d * (d ")) * (a "))) * (d * a)) * N by GROUP_1:def 3
.= ((a * ((1_ G) * (a "))) * (d * a)) * N by GROUP_1:def 5
.= ((a * (a ")) * (d * a)) * N by GROUP_1:def 4
.= ((1_ G) * (d * a)) * N by GROUP_1:def 5
.= (d * a) * N by GROUP_1:def 4 ;
hence S1 * S = S * S1 by A10, A11, A12; :: thesis: verum

end;

hence S1 in center (G ./. N) by GROUP_5:77; :: thesis: verum

end;

hence G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) by GROUP_2:58; :: thesis: verum