for O being set
for G being GroupWithOperators of O
for A being Subset of G
for g1 being Element of G holds
( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )