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 ;

now

set e = 1_ N;
reconsider e' = 1_ N as Element of H ;
take e' = e'; :: thesis: for h' being Element of H holds
( h' * e' = h' & e' * h' = h' & ex g' being Element of H st
( h' * g' = e' & g' * h' = e' ) )
let h' be Element of H; :: thesis: ( h' * e' = h' & e' * h' = h' & ex g' being Element of H st
( h' * g' = e' & g' * h' = e' ) )
reconsider h = h' as Element of N ;
h' * e' = h * (1_ N)
.= h by GROUP_1:def 5 ;
hence h' * e' = h' ; :: thesis: ( e' * h' = h' & ex g' being Element of H st
( h' * g' = e' & g' * h' = e' ) )
e' * h' = (1_ N) * h
.= h by GROUP_1:def 5 ;
hence e' * h' = h' ; :: thesis: ex g' being Element of H st
( h' * g' = e' & g' * h' = e' )
set g = h " ;
reconsider g' = h " as Element of H ;
take g' = g'; :: thesis: ( h' * g' = e' & g' * h' = e' )
h' * g' = h * (h " )
.= 1_ N by GROUP_1:def 6 ;
hence h' * g' = e' ; :: thesis: g' * h' = e'
g' * h' = (h " ) * h
.= 1_ N by GROUP_1:def 6 ;
hence g' * h' = e' ; :: thesis: verum

end;

then reconsider H = H as non empty Group-like multMagma by GROUP_1:def 3;
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