:: deftheorem defines |^ GROUP_3:def 5 :
for G being Group
for A being Subset of G
for g being Element of G holds g |^ A = {g} |^ A;