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 A1, GROUP_6:def 1;

reconsider K = N9 ./. ((N9,M9) `*`) as normal Subgroup of G ./. M9 by A2, GROUP_6:29;

.= the carrier of (N ./. MN) by Def14 ;

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

then reconsider f = CosOp MN99 as BinOp of (Cosets MN9) ;

.= 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: verum

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 A1, GROUP_6:def 1;

reconsider K = N9 ./. ((N9,M9) `*`) as normal Subgroup of G ./. M9 by A2, GROUP_6:29;

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 ) )

then A15: the carrier of K =
Cosets MN9
by TARSKI:2
( ( 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 ) )

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;

hence x in Cosets MN9 by GROUP_6:14; :: thesis: verum

end;hereby :: thesis: ( x in Cosets MN99 implies x in Cosets MN9 )

assume
x in Cosets MN99
; :: thesis: x in Cosets MN9assume
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;

hence x in Cosets MN99 by GROUP_6:14; :: thesis: verum

end;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 ) } ) )

then
x = a9 * MN99
by A5, TARSKI:2;( ( 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 ) } ) )

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;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 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 ) } 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;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

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

hence x in Cosets MN99 by GROUP_6:14; :: thesis: verum

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 ) } ) )

then
x = a * MN9
by A10, TARSKI:2;( ( 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 ) } ) )

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: verum

end;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 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 ) } 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 A3, A12; :: thesis: verum

end;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: verum

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: verum

hence x in Cosets MN9 by GROUP_6:14; :: thesis: verum

.= 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

A23:
the carrier of (G ./. M) = the carrier of (G ./. M9)
by Def14;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

end;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

hence
H is normal
by GROUP_3:118; :: thesis: verumlet a be Element of (G ./. M); :: thesis: a * H c= H * a

reconsider a9 = a as Element of (G ./. M9) by Def14;

end;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

hence
a * H c= H * a
; :: thesis: verumx 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 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:27, GROUP_3:118;

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 A21, Def15;

hence x in (carr H) * a by A15, A17, A22, GROUP_2:28; :: thesis: verum

end;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 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:27, GROUP_3:118;

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 A21, Def15;

hence x in (carr H) * a by A15, A17, A22, GROUP_2:28; :: thesis: verum

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

A25: now :: thesis: for o being Element of O holds (N ./. MN) ^ o = ((G ./. M) ^ o) | the carrier of (N ./. MN)

Cosets MN99 = Cosets MN9
by A4, TARSKI:2;let o be Element of O; :: thesis: (N ./. MN) ^ b_{1} = ((G ./. M) ^ b_{1}) | the carrier of (N ./. MN)

end;per cases
( not o in O or o in O )
;

end;

suppose A26:
not o in O
; :: thesis: (N ./. MN) ^ b_{1} = ((G ./. M) ^ b_{1}) | the carrier of (N ./. MN)

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

.= (id the carrier of (G ./. M)) | the carrier of (N ./. MN) by A28, A31

.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by A26, Def6 ; :: thesis: verum

end;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)

[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 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: verum

end;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 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: verum

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)

thus (N ./. MN) ^ o =
id the carrier of (N ./. MN)
by A26, Def6
[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 A32, RELAT_1:def 11;

hence [x,y] in id the carrier of (N ./. MN) by A33, RELAT_1:def 10; :: thesis: verum

end;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 A32, RELAT_1:def 11;

hence [x,y] in id the carrier of (N ./. MN) by A33, RELAT_1:def 10; :: thesis: verum

.= (id the carrier of (G ./. M)) | the carrier of (N ./. MN) by A28, A31

.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by A26, Def6 ; :: thesis: verum

suppose A34:
o in O
; :: thesis: (N ./. MN) ^ b_{1} = ((G ./. M) ^ b_{1}) | 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 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:5;

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;

.= f | the carrier of (N ./. MN) by A38, A40, A42, FUNCT_1:46

.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by A34, A35, Def6 ; :: thesis: verum

end;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:5;

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 :: thesis: for x being object st x in dom g holds

g . x = f . x

thus (N ./. MN) ^ o =
the action of (N ./. MN) . o
by A34, Def6
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 A44, XTUPLE_0:1;

[x,(f . x)] in f by A24, A36, A39, A43, FUNCT_1:1;

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, XTUPLE_0:1;

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, Lm8;

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, Lm8;

A64: B2 = g . x by A44, XTUPLE_0:1;

A65: B1 = f . x by A47, XTUPLE_0:1;

A29 = a2 * MN9 by A51, Lm8;

then (a1 ") * a29 in M9 by A49, A46, A58, A70, GROUP_2:114;

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 A57, GROUP_6:32;

b29 = ((G ^ o) | the carrier of N) . a2 by A53, Def7

.= (G ^ o) . a29 by FUNCT_1:49 ;

then (b1 ") * b29 in M by A72, A71, GROUP_6:def 6;

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, Lm8;

hence g . x = f . x by A65, A64, A63, A73, A54, GROUP_2:114; :: thesis: verum

end;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 A44, XTUPLE_0:1;

[x,(f . x)] in f by A24, A36, A39, A43, FUNCT_1:1;

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, XTUPLE_0:1;

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, Lm8;

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, Lm8;

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) ) )

then A63:
b29 * M9 = b2 * MN9
by TARSKI:2;( ( 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) ) )

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 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:27; :: thesis: verum

end;hereby :: thesis: ( x in b29 * (carr M9) implies x in b2 * (carr MN9) )

assume
x in b29 * (carr M9)
; :: thesis: 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 A59, Th3;

hence x in b29 * (carr M9) by A1, A60, GROUP_2:27; :: thesis: verum

end;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 A59, Th3;

hence x in b29 * (carr M9) by A1, A60, GROUP_2:27; :: thesis: verum

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 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:27; :: thesis: verum

A64: B2 = g . x by A44, XTUPLE_0:1;

A65: B1 = f . x by A47, XTUPLE_0:1;

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) ) )

then A70:
a2 * MN9 = a29 * M9
by TARSKI:2;( ( 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) ) )

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 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:27; :: thesis: verum

end;hereby :: thesis: ( x in a29 * (carr M9) implies x in a2 * (carr MN9) )

assume
x in a29 * (carr M9)
; :: thesis: 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 A66, Th3;

hence x in a29 * (carr M9) by A1, A67, GROUP_2:27; :: thesis: verum

end;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 A66, Th3;

hence x in a29 * (carr M9) by A1, A67, GROUP_2:27; :: thesis: verum

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 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:27; :: thesis: verum

A29 = a2 * MN9 by A51, Lm8;

then (a1 ") * a29 in M9 by A49, A46, A58, A70, GROUP_2:114;

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 A57, GROUP_6:32;

b29 = ((G ^ o) | the carrier of N) . a2 by A53, Def7

.= (G ^ o) . a29 by FUNCT_1:49 ;

then (b1 ") * b29 in M by A72, A71, GROUP_6:def 6;

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, Lm8;

hence g . x = f . x by A65, A64, A63, A73, A54, GROUP_2:114; :: thesis: verum

.= f | the carrier of (N ./. MN) by A38, A40, A42, FUNCT_1:46

.= ((G ./. M) ^ o) | the carrier of (N ./. MN) by A34, A35, Def6 ; :: thesis: verum

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

then the multF of K =
CosOp MN9
by GROUP_6:def 3
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

.= A19 * A29 by A74, A75, GROUP_6:def 3

.= A1 * A2 by A76, TARSKI:2 ; :: thesis: verum

end;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 ) )

thus f . (W1,W2) =
f . (W19,W29)
( ( 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 ) )

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;hereby :: thesis: ( x in A19 * A29 implies x in A1 * A2 )

assume
x in A19 * A29
; :: thesis: x in A1 * A2assume
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;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

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

.= A19 * A29 by A74, A75, GROUP_6:def 3

.= A1 * A2 by A76, TARSKI:2 ; :: thesis: verum

.= 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: verum