theorem Th43: :: GROUP_9:43

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds 1_ (G ./. N) = carr N