theorem :: GROUP_9:69

for O being set
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 by Lm6;