for G being Group
for a being Element of G holds (<*> the carrier of G) |^ a = {}