:: deftheorem defines is_fixed_under GROUP_10:def 12 :
for S being non empty unital multMagma
for E being set
for T being LeftOperation of S,E
for x being Element of E holds
( x is_fixed_under T iff for s being Element of S holds x = (T ^ s) . x );