let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let M, N be strict normal StableSubgroup of G; :: thesis:
reconsider M9 = multMagma(# the carrier of M,the multF of M #) as normal Subgroup of G by Lm7;
reconsider N9 = multMagma(# the carrier of N,the multF of N #) as normal Subgroup of G by Lm7;
let MN be normal StableSubgroup of N; :: thesis:
assume A1: MN = M ; :: thesis:
reconsider MN99 = N9,M9 `*` as normal Subgroup of N9 ;
reconsider MN9 = multMagma(# the carrier of MN,the multF of MN #) as normal Subgroup of N by Lm7;
assume M is StableSubgroup of N ; :: thesis:
then M is Subgroup of N by Def7;
then ( the carrier of M c= the carrier of N & the multF of M = the multF of N || the carrier of M ) by GROUP_2:def 5;
then A2: M9 is Subgroup of N9 by GROUP_2:def 5;
then A3: N9,M9 `*` = MN9 by A1, GROUP_6:def 1;
reconsider K = N9 ./. (N9,M9 `*` ) as normal Subgroup of G ./. M9 by A2, GROUP_6:35;

A4: now

let x be set ; :: thesis:

hereby :: thesis:

assume x in Cosets MN9 ; :: thesis:
then consider a being Element of N such that
A5: x = a * MN9 and
x = MN9 * a by GROUP_6:15;
reconsider a9 = a as Element of N9 ;
reconsider A = {a} as Subset of N by ZFMISC_1:37;
reconsider A9 = {a9} as Subset of N9 by ZFMISC_1:37;

now

let y be set ; :: thesis:

hereby :: thesis:

assume y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } ; :: thesis:
then consider g, h being Element of N such that
A6: y = g * h and
A7: ( g in A & h in carr MN9 ) ;
reconsider h9 = h as Element of N9 ;
reconsider g9 = g as Element of N9 ;
y = g9 * h9 by A6;
hence y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } by A3, A7; :: thesis:

end;

assume y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } ; :: thesis:
then consider g, h being Element of N9 such that
A8: y = g * h and
A9: ( g in A9 & h in carr MN99 ) ;
reconsider h9 = h as Element of N ;
reconsider g9 = g as Element of N ;
y = g9 * h9 by A8;
hence y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } by A3, A9; :: thesis:

end;

then x = a9 * MN99 by A5, TARSKI:2;
hence x in Cosets MN99 by GROUP_6:16; :: thesis:

end;

assume x in Cosets MN99 ; :: thesis:
then consider a9 being Element of N9 such that
A10: x = a9 * MN99 and
x = MN99 * a9 by GROUP_6:15;
reconsider a = a9 as Element of N ;
reconsider A9 = {a9} as Subset of N9 by ZFMISC_1:37;
reconsider A = {a} as Subset of N by ZFMISC_1:37;

now

let y be set ; :: thesis:

hereby :: thesis:

assume y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } ; :: thesis:
then consider g, h being Element of N such that
A11: y = g * h and
A12: ( g in A & h in carr MN9 ) ;
reconsider h9 = h as Element of N9 ;
reconsider g9 = g as Element of N9 ;
y = g9 * h9 by A11;
hence y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } by A3, A12; :: thesis:

end;

assume y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } ; :: thesis:
then consider g, h being Element of N9 such that
A13: y = g * h and
A14: ( g in A9 & h in carr MN99 ) ;
reconsider h9 = h as Element of N ;
reconsider g9 = g as Element of N ;
y = g9 * h9 by A13;
hence y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } by A3, A14; :: thesis:

end;

then x = a * MN9 by A10, TARSKI:2;
hence x in Cosets MN9 by GROUP_6:16; :: thesis:

end;

then A15: the carrier of K = Cosets MN9 by TARSKI:2
.= the carrier of (N ./. MN) by Def14 ;

A16: now

let H be strict Subgroup of G ./. M; :: thesis:
assume A17: H = multMagma(# the carrier of (N ./. MN),the multF of (N ./. MN) #) ; :: thesis:

now

let a be Element of (G ./. M); :: thesis:
reconsider a9 = a as Element of (G ./. M9) by Def14;

now

let x be set ; :: thesis:
assume x in a * (carr H) ; :: thesis:
then consider b being Element of (G ./. M) such that
A18: x = a * b and
A19: b in carr H by GROUP_2:33;
reconsider b9 = b as Element of (G ./. M9) by Def14;
A20: x = a9 * b9 by A18, Def15;
then reconsider x9 = x as Element of (G ./. M9) ;
( a9 * K c= K * a9 & x9 in a9 * (carr K) ) by A15, A17, A19, A20, GROUP_2:33, GROUP_3:141;
then consider c9 being Element of (G ./. M9) such that
A21: x9 = c9 * a9 and
A22: c9 in carr K by GROUP_2:34;
reconsider c = c9 as Element of (G ./. M) by Def14;
x = c * a by A21, Def15;
hence x in (carr H) * a by A15, A17, A22, GROUP_2:34; :: thesis:

end;

hence a * H c= H * a by TARSKI:def 3; :: thesis:

end;

hence H is normal by GROUP_3:141; :: thesis:

end;

A23: the carrier of (G ./. M) = the carrier of (G ./. M9) by Def14;
then A24: the carrier of (N ./. MN) c= the carrier of (G ./. M) by A15, GROUP_2:def 5;

A25: now

let o be Element of O; :: thesis:

per cases ;

suppose A26: not o in O ; :: thesis:

A27: the carrier of (N ./. MN) c= the carrier of (G ./. M) by A23, A15, GROUP_2:def 5;

A28: now

let x, y be set ; :: thesis:
assume A29: [x,y] in id the carrier of (N ./. MN) ; :: thesis:
then A30: x in the carrier of (N ./. MN) by RELAT_1:def 10;
x = y by A29, RELAT_1:def 10;
then [x,y] in id the carrier of (G ./. M) by A27, A30, RELAT_1:def 10;
hence [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) by A30, RELAT_1:def 11; :: thesis:

end;

A31: now

let x, y be set ; :: thesis:
assume A32: [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) ; :: thesis:
then [x,y] in id the carrier of (G ./. M) by RELAT_1:def 11;
then A33: x = y by RELAT_1:def 10;
x in the carrier of (N ./. MN) by A32, RELAT_1:def 11;
hence [x,y] in id the carrier of (N ./. MN) by A33, RELAT_1:def 10; :: thesis:

end;

thus (N ./. MN) ^ o = id the carrier of (N ./. MN) by A26, Def6
.= (id the carrier of (G ./. M)) | the carrier of (N ./. MN) by A28, A31, RELAT_1:def 2
.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by A26, Def6 ; :: thesis:

end;

suppose A34: o in O ; :: thesis:

then the action of (G ./. M) . o in Funcs the carrier of (G ./. M),the carrier of (G ./. M) by FUNCT_2:7;
then consider f being Function such that
A35: f = the action of (G ./. M) . o and
A36: dom f = the carrier of (G ./. M) and
rng f c= the carrier of (G ./. M) by FUNCT_2:def 2;
A37: f = { [A,B] where A, B is Element of Cosets M : ex a, b being Element of G st
( a in A & b in B & b = (G ^ o) . a ) } by A34, A35, Def16;
the action of (N ./. MN) . o in Funcs the carrier of (N ./. MN),the carrier of (N ./. MN) by A34, FUNCT_2:7;
then consider g being Function such that
A38: g = the action of (N ./. MN) . o and
A39: dom g = the carrier of (N ./. MN) and
rng g c= the carrier of (N ./. MN) by FUNCT_2:def 2;
A40: dom g = (dom f) /\ the carrier of (N ./. MN) by A24, A36, A39, XBOOLE_1:28;
A41: g = { [A,B] where A, B is Element of Cosets MN : ex a, b being Element of N st
( a in A & b in B & b = (N ^ o) . a ) } by A34, A38, Def16;

A42: now

let x be set ; :: thesis:
assume A43: x in dom g ; :: thesis:
then [x,(g . x)] in g by FUNCT_1:8;
then consider A2, B2 being Element of Cosets MN such that
A44: [x,(g . x)] = [A2,B2] and
A45: ex a, b being Element of N st
( a in A2 & b in B2 & b = (N ^ o) . a ) by A41;
A46: A2 = x by A44, ZFMISC_1:33;
[x,(f . x)] in f by A24, A36, A39, A43, FUNCT_1:8;
then consider A1, B1 being Element of Cosets M such that
A47: [x,(f . x)] = [A1,B1] and
A48: ex a, b being Element of G st
( a in A1 & b in B1 & b = (G ^ o) . a ) by A37;
A49: A1 = x by A47, ZFMISC_1:33;
reconsider A29 = A2, B29 = B2 as Element of Cosets MN9 by Def14;
reconsider A19 = A1, B19 = B1 as Element of Cosets M9 by Def14;
set fo = G ^ o;
N is Subgroup of G by Def7;
then A50: the carrier of N c= the carrier of G by GROUP_2:def 5;
consider a2, b2 being Element of N such that
A51: a2 in A2 and
A52: b2 in B2 and
A53: b2 = (N ^ o) . a2 by A45;
A54: B29 = b2 * MN9 by A52, Lm9;
( a2 in the carrier of N & b2 in the carrier of N ) ;
then reconsider a29 = a2, b29 = b2 as Element of G by A50;
consider a1, b1 being Element of G such that
A55: a1 in A1 and
A56: b1 in B1 and
A57: b1 = (G ^ o) . a1 by A48;
A58: A19 = a1 * M9 by A55, Lm9;

now

let x be set ; :: thesis:

hereby :: thesis:

assume x in b2 * (carr MN9) ; :: thesis:
then consider h being Element of N such that
A59: x = b2 * h and
A60: h in carr MN9 by GROUP_2:33;
h in the carrier of N ;
then reconsider h9 = h as Element of G by A50;
x = b29 * h9 by A59, Th3;
hence x in b29 * (carr M9) by A1, A60, GROUP_2:33; :: thesis:

end;

assume x in b29 * (carr M9) ; :: thesis:
then consider h being Element of G such that
A61: x = b29 * h and
A62: h in carr M9 by GROUP_2:33;
h in carr MN9 by A1, A62;
then reconsider h9 = h as Element of N ;
x = b2 * h9 by A61, Th3;
hence x in b2 * (carr MN9) by A1, A62, GROUP_2:33; :: thesis:

end;

then A63: b29 * M9 = b2 * MN9 by TARSKI:2;
A64: B2 = g . x by A44, ZFMISC_1:33;
A65: B1 = f . x by A47, ZFMISC_1:33;

now

let x be set ; :: thesis:

hereby :: thesis:

assume x in a2 * (carr MN9) ; :: thesis:
then consider h being Element of N such that
A66: x = a2 * h and
A67: h in carr MN9 by GROUP_2:33;
h in the carrier of N ;
then reconsider h9 = h as Element of G by A50;
x = a29 * h9 by A66, Th3;
hence x in a29 * (carr M9) by A1, A67, GROUP_2:33; :: thesis:

end;

assume x in a29 * (carr M9) ; :: thesis:
then consider h being Element of G such that
A68: x = a29 * h and
A69: h in carr M9 by GROUP_2:33;
h in carr MN9 by A1, A69;
then reconsider h9 = h as Element of N ;
x = a2 * h9 by A68, Th3;
hence x in a2 * (carr MN9) by A1, A69, GROUP_2:33; :: thesis:

end;

then A70: a2 * MN9 = a29 * M9 by TARSKI:2;
A29 = a2 * MN9 by A51, Lm9;
then (a1 " ) * a29 in M9 by A49, A46, A58, A70, GROUP_2:137;
then (a1 " ) * a29 in the carrier of M by STRUCT_0:def 5;
then (a1 " ) * a29 in M by STRUCT_0:def 5;
then A71: (G ^ o) . ((a1 " ) * a29) in M by Lm10;
A72: b1 " = (G ^ o) . (a1 " ) by A57, GROUP_6:41;
b29 = ((G ^ o) | the carrier of N) . a2 by A53, Def7
.= (G ^ o) . a29 by FUNCT_1:72 ;
then (b1 " ) * b29 in M by A72, A71, GROUP_6:def 7;
then (b1 " ) * b29 in the carrier of M by STRUCT_0:def 5;
then A73: (b1 " ) * b29 in M9 by STRUCT_0:def 5;
B19 = b1 * M9 by A56, Lm9;
hence g . x = f . x by A65, A64, A63, A73, A54, GROUP_2:137; :: thesis:

end;

thus (N ./. MN) ^ o = the action of (N ./. MN) . o by A34, Def6
.= f | the carrier of (N ./. MN) by A38, A40, A42, FUNCT_1:68
.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by A34, A35, Def6 ; :: thesis:

end;

Cosets MN99 = Cosets MN9 by A4, TARSKI:2;
then reconsider f = CosOp MN99 as BinOp of (Cosets MN9) ;

now

let W1, W2 be Element of Cosets MN9; :: thesis:
reconsider W19 = W1, W29 = W2 as Element of Cosets MN99 by A4;
let A1, A2 be Subset of N; :: thesis:
assume A74: W1 = A1 ; :: thesis:
reconsider A19 = A1, A29 = A2 as Subset of N9 ;
assume A75: W2 = A2 ; :: thesis:

A76: now

let x be set ; :: thesis:

hereby :: thesis:

assume x in A1 * A2 ; :: thesis:
then consider g, h being Element of N such that
A77: x = g * h and
A78: ( g in A1 & h in A2 ) ;
reconsider g9 = g, h9 = h as Element of N9 ;
x = g9 * h9 by A77;
hence x in A19 * A29 by A78; :: thesis:

end;

assume x in A19 * A29 ; :: thesis:
then consider g9, h9 being Element of N9 such that
A79: x = g9 * h9 and
A80: ( g9 in A19 & h9 in A29 ) ;
reconsider g = g9, h = h9 as Element of N ;
x = g * h by A79;
hence x in A1 * A2 by A80; :: thesis:

end;

thus f . W1,W2 = f . W19,W29
.= A19 * A29 by A74, A75, GROUP_6:def 4
.= A1 * A2 by A76, TARSKI:2 ; :: thesis:

end;

then the multF of K = CosOp MN9 by GROUP_6:def 4
.= the multF of (N ./. MN) by Def15 ;
then the multF of (N ./. MN) = the multF of (G ./. M9) || the carrier of K by GROUP_2:def 5
.= the multF of (G ./. M) || the carrier of (N ./. MN) by A15, Def15 ;
then N ./. MN is Subgroup of G ./. M by A24, GROUP_2:def 5;
hence N ./. MN is normal StableSubgroup of G ./. M by A16, A25, Def7, Def10; :: thesis: