theorem Th76: :: GROUP_9:76

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds
HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)