:: deftheorem Def1 defines being_left_operation GROUP_10:def 1 :
for S being non empty unital multMagma
for E being set
for A being Action of the carrier of S,E holds
( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) );