let O be set ; :: thesis: for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds

( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G

for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds

( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

let N be normal StableSubgroup of G; :: thesis: for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds

( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

let N9 be normal Subgroup of G; :: thesis: ( N9 = multMagma(# the carrier of N, the multF of N #) implies ( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) ) )

assume A1: N9 = multMagma(# the carrier of N, the multF of N #) ; :: thesis: ( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

then reconsider e = 1_ (G ./. N9) as Element of (G ./. N) by Def14;

Cosets N9 = Cosets N by A1, Def14;

hence G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) by A1, Def15; :: thesis: 1_ (G ./. N9) = 1_ (G ./. N)

for N being normal StableSubgroup of G

for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds

( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G

for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds

( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

let N be normal StableSubgroup of G; :: thesis: for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds

( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

let N9 be normal Subgroup of G; :: thesis: ( N9 = multMagma(# the carrier of N, the multF of N #) implies ( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) ) )

assume A1: N9 = multMagma(# the carrier of N, the multF of N #) ; :: thesis: ( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

then reconsider e = 1_ (G ./. N9) as Element of (G ./. N) by Def14;

Cosets N9 = Cosets N by A1, Def14;

hence G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) by A1, Def15; :: thesis: 1_ (G ./. N9) = 1_ (G ./. N)

now :: thesis: for h being Element of (G ./. N) holds

( h * e = h & e * h = h )

hence
1_ (G ./. N9) = 1_ (G ./. N)
by GROUP_1:4; :: thesis: verum( h * e = h & e * h = h )

let h be Element of (G ./. N); :: thesis: ( h * e = h & e * h = h )

reconsider h9 = h as Element of (G ./. N9) by A1, Def14;

thus h * e = h9 * (1_ (G ./. N9)) by A1, Def15

.= h by GROUP_1:def 4 ; :: thesis: e * h = h

thus e * h = (1_ (G ./. N9)) * h9 by A1, Def15

.= h by GROUP_1:def 4 ; :: thesis: verum

end;reconsider h9 = h as Element of (G ./. N9) by A1, Def14;

thus h * e = h9 * (1_ (G ./. N9)) by A1, Def15

.= h by GROUP_1:def 4 ; :: thesis: e * h = h

thus e * h = (1_ (G ./. N9)) * h9 by A1, Def15

.= h by GROUP_1:def 4 ; :: thesis: verum