for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G
for h1 being Element of H1 st h1 = g1 holds
h1 " = g1 "