theorem Th75: :: GROUP_9:75

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)