theorem :: GROUP_9:74

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds
( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) ) by Lm34;