let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let N be normal StableSubgroup of G; :: thesis:
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 ;

set e = 1_ N;
reconsider e9 = 1_ N as Element of H ;
take e9 = e9; :: thesis:
let h9 be Element of H; :: thesis:
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 = (1_ N) * h
.= h by GROUP_1:def 4 ;
hence e9 * h9 = h9 ; :: thesis:
take g9 = g9; :: thesis:
h9 * g9 = h * (h ")
.= 1_ N by GROUP_1:def 5 ;
hence h9 * g9 = e9 ; :: thesis:
g9 * h9 = (h ") * h
.= 1_ N by GROUP_1:def 5 ;
hence g9 * h9 = e9 ; :: thesis:

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: