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

for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

let N be normal StableSubgroup of G; :: thesis: multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

set H = multMagma(# the carrier of N, the multF of N #);

reconsider H = multMagma(# the carrier of N, the multF of N #) as non empty multMagma ;

N is Subgroup of G by Def7;

then ( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def 5;

then reconsider H = H as Subgroup of G by GROUP_2:def 5;

H is normal by Def10;

hence multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G ; :: thesis: verum

for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

let N be normal StableSubgroup of G; :: thesis: multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

set H = multMagma(# the carrier of N, the multF of N #);

reconsider H = multMagma(# the carrier of N, the multF of N #) as non empty multMagma ;

now :: thesis: ex e9 being Element of H st

for h9 being Element of H holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

then reconsider H = H as non empty Group-like multMagma by GROUP_1:def 2;for h9 being Element of H holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

set e = 1_ N;

reconsider e9 = 1_ N as Element of H ;

take e9 = e9; :: thesis: for h9 being Element of H holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

let h9 be Element of H; :: thesis: ( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

reconsider h = h9 as Element of N ;

set g = h " ;

reconsider g9 = h " as Element of H ;

h9 * e9 = h * (1_ N)

.= h by GROUP_1:def 4 ;

hence h9 * e9 = h9 ; :: thesis: ( e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

e9 * h9 = (1_ N) * h

.= h by GROUP_1:def 4 ;

hence e9 * h9 = h9 ; :: thesis: ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 )

take g9 = g9; :: thesis: ( h9 * g9 = e9 & g9 * h9 = e9 )

h9 * g9 = h * (h ")

.= 1_ N by GROUP_1:def 5 ;

hence h9 * g9 = e9 ; :: thesis: g9 * h9 = e9

g9 * h9 = (h ") * h

.= 1_ N by GROUP_1:def 5 ;

hence g9 * h9 = e9 ; :: thesis: verum

end;reconsider e9 = 1_ N as Element of H ;

take e9 = e9; :: thesis: for h9 being Element of H holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

let h9 be Element of H; :: thesis: ( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

reconsider h = h9 as Element of N ;

set g = h " ;

reconsider g9 = h " as Element of H ;

h9 * e9 = h * (1_ N)

.= h by GROUP_1:def 4 ;

hence h9 * e9 = h9 ; :: thesis: ( e9 * h9 = h9 & ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

e9 * h9 = (1_ N) * h

.= h by GROUP_1:def 4 ;

hence e9 * h9 = h9 ; :: thesis: ex g9 being Element of H st

( h9 * g9 = e9 & g9 * h9 = e9 )

take g9 = g9; :: thesis: ( h9 * g9 = e9 & g9 * h9 = e9 )

h9 * g9 = h * (h ")

.= 1_ N by GROUP_1:def 5 ;

hence h9 * g9 = e9 ; :: thesis: g9 * h9 = e9

g9 * h9 = (h ") * h

.= 1_ N by GROUP_1:def 5 ;

hence g9 * h9 = e9 ; :: thesis: verum

N is Subgroup of G by Def7;

then ( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def 5;

then reconsider H = H as Subgroup of G by GROUP_2:def 5;

H is normal by Def10;

hence multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G ; :: thesis: verum