theorem :: GROUP_9:70

for O being set
for o being Element of O
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G st g1 in H1 holds
(G ^ o) . g1 in H1 by Lm9;