let O be set ; :: thesis: for G being GroupWithOperators of O
for M, N being strict normal StableSubgroup of G
for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M

let G be GroupWithOperators of O; :: thesis: for M, N being strict normal StableSubgroup of G
for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M

let M, N be strict normal StableSubgroup of G; :: thesis: for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M

reconsider M9 = multMagma(# the carrier of M, the multF of M #) as normal Subgroup of G by Lm6;
reconsider N9 = multMagma(# the carrier of N, the multF of N #) as normal Subgroup of G by Lm6;
let MN be normal StableSubgroup of N; :: thesis: ( MN = M & M is StableSubgroup of N implies N ./. MN is normal StableSubgroup of G ./. M )
assume A1: MN = M ; :: thesis: ( not M is StableSubgroup of N or N ./. MN is normal StableSubgroup of G ./. M )
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 Lm6;
assume M is StableSubgroup of N ; :: thesis: N ./. MN is normal StableSubgroup of G ./. M
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 ;
reconsider K = N9 ./. ((N9,M9) `*`) as normal Subgroup of G ./. M9 by ;
A4: now :: thesis: for x being object holds
( ( x in Cosets MN9 implies x in Cosets MN99 ) & ( x in Cosets MN99 implies x in Cosets MN9 ) )
let x be object ; :: thesis: ( ( x in Cosets MN9 implies x in Cosets MN99 ) & ( x in Cosets MN99 implies x in Cosets MN9 ) )
hereby :: thesis: ( x in Cosets MN99 implies x in Cosets MN9 )
assume x in Cosets MN9 ; :: thesis: x in Cosets MN99
then consider a being Element of N such that
A5: x = a * MN9 and
x = MN9 * a by GROUP_6:13;
reconsider a9 = a as Element of N9 ;
reconsider A = {a} as Subset of N by ZFMISC_1:31;
reconsider A9 = {a9} as Subset of N9 by ZFMISC_1:31;
now :: thesis: for y being object holds
( ( y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } implies y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } ) & ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } ) )
let y be object ; :: thesis: ( ( y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } implies y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } ) & ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } ) )
hereby :: thesis: ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } )
assume y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } ; :: thesis: y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) }
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: verum
end;
assume y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } ; :: thesis: y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) }
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: verum
end;
then x = a9 * MN99 by ;
hence x in Cosets MN99 by GROUP_6:14; :: thesis: verum
end;
assume x in Cosets MN99 ; :: thesis: x in Cosets MN9
then consider a9 being Element of N9 such that
A10: x = a9 * MN99 and
x = MN99 * a9 by GROUP_6:13;
reconsider a = a9 as Element of N ;
reconsider A9 = {a9} as Subset of N9 by ZFMISC_1:31;
reconsider A = {a} as Subset of N by ZFMISC_1:31;
now :: thesis: for y being object holds
( ( y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } implies y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } ) & ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } ) )
let y be object ; :: thesis: ( ( y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } implies y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } ) & ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } ) )
hereby :: thesis: ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } )
assume y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } ; :: thesis: y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) }
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 ; :: thesis: verum
end;
assume y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } ; :: thesis: y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) }
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 ; :: thesis: verum
end;
then x = a * MN9 by ;
hence x in Cosets MN9 by GROUP_6:14; :: thesis: verum
end;
then A15: the carrier of K = Cosets MN9 by TARSKI:2
.= the carrier of (N ./. MN) by Def14 ;
A16: now :: thesis: for H being strict Subgroup of G ./. M st H = multMagma(# the carrier of (N ./. MN), the multF of (N ./. MN) #) holds
H is normal
let H be strict Subgroup of G ./. M; :: thesis: ( H = multMagma(# the carrier of (N ./. MN), the multF of (N ./. MN) #) implies H is normal )
assume A17: H = multMagma(# the carrier of (N ./. MN), the multF of (N ./. MN) #) ; :: thesis: H is normal
now :: thesis: for a being Element of (G ./. M) holds a * H c= H * a
let a be Element of (G ./. M); :: thesis: a * H c= H * a
reconsider a9 = a as Element of (G ./. M9) by Def14;
now :: thesis: for x being object st x in a * (carr H) holds
x in (carr H) * a
let x be object ; :: thesis: ( x in a * (carr H) implies x in (carr H) * a )
assume x in a * (carr H) ; :: thesis: x in (carr H) * a
then consider b being Element of (G ./. M) such that
A18: x = a * b and
A19: b in carr H by GROUP_2:27;
reconsider b9 = b as Element of (G ./. M9) by Def14;
A20: x = a9 * b9 by ;
then reconsider x9 = x as Element of (G ./. M9) ;
( a9 * K c= K * a9 & x9 in a9 * (carr K) ) by ;
then consider c9 being Element of (G ./. M9) such that
A21: x9 = c9 * a9 and
A22: c9 in carr K by GROUP_2:28;
reconsider c = c9 as Element of (G ./. M) by Def14;
x = c * a by ;
hence x in (carr H) * a by ; :: thesis: verum
end;
hence a * H c= H * a ; :: thesis: verum
end;
hence H is normal by GROUP_3:118; :: thesis: verum
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 ;
A25: now :: thesis: for o being Element of O holds (N ./. MN) ^ o = ((G ./. M) ^ o) | the carrier of (N ./. MN)
let o be Element of O; :: thesis: (N ./. MN) ^ b1 = ((G ./. M) ^ b1) | the carrier of (N ./. MN)
per cases ( not o in O or o in O ) ;
suppose A26: not o in O ; :: thesis: (N ./. MN) ^ b1 = ((G ./. M) ^ b1) | the carrier of (N ./. MN)
A27: the carrier of (N ./. MN) c= the carrier of (G ./. M) by ;
A28: now :: thesis: for x, y being object st [x,y] in id the carrier of (N ./. MN) holds
[x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN)
let x, y be object ; :: thesis: ( [x,y] in id the carrier of (N ./. MN) implies [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) )
assume A29: [x,y] in id the carrier of (N ./. MN) ; :: thesis: [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN)
then A30: x in the carrier of (N ./. MN) by RELAT_1:def 10;
x = y by ;
then [x,y] in id the carrier of (G ./. M) by ;
hence [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) by ; :: thesis: verum
end;
A31: now :: thesis: for x, y being object st [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) holds
[x,y] in id the carrier of (N ./. MN)
let x, y be object ; :: thesis: ( [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) implies [x,y] in id the carrier of (N ./. MN) )
assume A32: [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) ; :: thesis: [x,y] in id the carrier of (N ./. MN)
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 ;
hence [x,y] in id the carrier of (N ./. MN) by ; :: thesis: verum
end;
thus (N ./. MN) ^ o = id the carrier of (N ./. MN) by
.= (id the carrier of (G ./. M)) | the carrier of (N ./. MN) by
.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by ; :: thesis: verum
end;
suppose A34: o in O ; :: thesis: (N ./. MN) ^ b1 = ((G ./. M) ^ b1) | the carrier of (N ./. MN)
then the action of (G ./. M) . o in Funcs ( the carrier of (G ./. M), the carrier of (G ./. M)) by FUNCT_2:5;
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 ;
the action of (N ./. MN) . o in Funcs ( the carrier of (N ./. MN), the carrier of (N ./. MN)) by ;
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 ;
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 ;
A42: now :: thesis: for x being object st x in dom g holds
g . x = f . x
let x be object ; :: thesis: ( x in dom g implies g . x = f . x )
assume A43: x in dom g ; :: thesis: g . x = f . x
then [x,(g . x)] in g by FUNCT_1:1;
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 ;
[x,(f . x)] in f by ;
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 ;
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 ;
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 ;
now :: thesis: for x being object holds
( ( x in b2 * (carr MN9) implies x in b29 * (carr M9) ) & ( x in b29 * (carr M9) implies x in b2 * (carr MN9) ) )
let x be object ; :: thesis: ( ( x in b2 * (carr MN9) implies x in b29 * (carr M9) ) & ( x in b29 * (carr M9) implies x in b2 * (carr MN9) ) )
hereby :: thesis: ( x in b29 * (carr M9) implies x in b2 * (carr MN9) )
assume x in b2 * (carr MN9) ; :: thesis: x in b29 * (carr M9)
then consider h being Element of N such that
A59: x = b2 * h and
A60: h in carr MN9 by GROUP_2:27;
reconsider h9 = h as Element of G by A50;
x = b29 * h9 by ;
hence x in b29 * (carr M9) by ; :: thesis: verum
end;
assume x in b29 * (carr M9) ; :: thesis: x in b2 * (carr MN9)
then consider h being Element of G such that
A61: x = b29 * h and
A62: h in carr M9 by GROUP_2:27;
h in carr MN9 by ;
then reconsider h9 = h as Element of N ;
x = b2 * h9 by ;
hence x in b2 * (carr MN9) by ; :: thesis: verum
end;
then A63: b29 * M9 = b2 * MN9 by TARSKI:2;
A64: B2 = g . x by ;
A65: B1 = f . x by ;
now :: thesis: for x being object holds
( ( x in a2 * (carr MN9) implies x in a29 * (carr M9) ) & ( x in a29 * (carr M9) implies x in a2 * (carr MN9) ) )
let x be object ; :: thesis: ( ( x in a2 * (carr MN9) implies x in a29 * (carr M9) ) & ( x in a29 * (carr M9) implies x in a2 * (carr MN9) ) )
hereby :: thesis: ( x in a29 * (carr M9) implies x in a2 * (carr MN9) )
assume x in a2 * (carr MN9) ; :: thesis: x in a29 * (carr M9)
then consider h being Element of N such that
A66: x = a2 * h and
A67: h in carr MN9 by GROUP_2:27;
reconsider h9 = h as Element of G by A50;
x = a29 * h9 by ;
hence x in a29 * (carr M9) by ; :: thesis: verum
end;
assume x in a29 * (carr M9) ; :: thesis: x in a2 * (carr MN9)
then consider h being Element of G such that
A68: x = a29 * h and
A69: h in carr M9 by GROUP_2:27;
h in carr MN9 by ;
then reconsider h9 = h as Element of N ;
x = a2 * h9 by ;
hence x in a2 * (carr MN9) by ; :: thesis: verum
end;
then A70: a2 * MN9 = a29 * M9 by TARSKI:2;
A29 = a2 * MN9 by ;
then (a1 ") * a29 in M9 by ;
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 Lm9;
A72: b1 " = (G ^ o) . (a1 ") by ;
b29 = ((G ^ o) | the carrier of N) . a2 by
.= (G ^ o) . a29 by FUNCT_1:49 ;
then (b1 ") * b29 in M by ;
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 ;
hence g . x = f . x by ; :: thesis: verum
end;
thus (N ./. MN) ^ o = the action of (N ./. MN) . o by
.= f | the carrier of (N ./. MN) by
.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by ; :: thesis: verum
end;
end;
end;
Cosets MN99 = Cosets MN9 by ;
then reconsider f = CosOp MN99 as BinOp of (Cosets MN9) ;
now :: thesis: for W1, W2 being Element of Cosets MN9
for A1, A2 being Subset of N st W1 = A1 & W2 = A2 holds
f . (W1,W2) = A1 * A2
let W1, W2 be Element of Cosets MN9; :: thesis: for A1, A2 being Subset of N st W1 = A1 & W2 = A2 holds
f . (W1,W2) = A1 * A2

reconsider W19 = W1, W29 = W2 as Element of Cosets MN99 by A4;
let A1, A2 be Subset of N; :: thesis: ( W1 = A1 & W2 = A2 implies f . (W1,W2) = A1 * A2 )
assume A74: W1 = A1 ; :: thesis: ( W2 = A2 implies f . (W1,W2) = A1 * A2 )
reconsider A19 = A1, A29 = A2 as Subset of N9 ;
assume A75: W2 = A2 ; :: thesis: f . (W1,W2) = A1 * A2
A76: now :: thesis: for x being object holds
( ( x in A1 * A2 implies x in A19 * A29 ) & ( x in A19 * A29 implies x in A1 * A2 ) )
let x be object ; :: thesis: ( ( x in A1 * A2 implies x in A19 * A29 ) & ( x in A19 * A29 implies x in A1 * A2 ) )
hereby :: thesis: ( x in A19 * A29 implies x in A1 * A2 )
assume x in A1 * A2 ; :: thesis: x in A19 * A29
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: verum
end;
assume x in A19 * A29 ; :: thesis: x in A1 * A2
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: verum
end;
thus f . (W1,W2) = f . (W19,W29)
.= A19 * A29 by
.= A1 * A2 by ; :: thesis: verum
end;
then the multF of K = CosOp MN9 by GROUP_6:def 3
.= 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 ;
then N ./. MN is Subgroup of G ./. M by ;
hence N ./. MN is normal StableSubgroup of G ./. M by ; :: thesis: verum