let O, E be set ; :: thesis: for A being Action of O,E holds [#] E is_stable_under_the_action_of A
let A be Action of O,E; :: thesis: [#] E is_stable_under_the_action_of A
for o being Element of O
for f being Function of E,E st o in O & f = A . o holds
f .: ([#] E) c= [#] E ;
hence [#] E is_stable_under_the_action_of A by Def1; :: thesis: verum