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

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;

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