theorem :: GROUP_9:65

for O, E being set
for A being Action of O,E
for F being FinSequence of O
for Y being Subset of E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y by Lm29;