:: deftheorem Def6 defines ^ GROUP_9:def 6 :
for O being set
for G being GroupWithOperators of O
for o being Element of O holds
( ( o in O implies G ^ o = the action of G . o ) & ( not o in O implies G ^ o = id the carrier of G ) );