for G being finite Group
for a being Element of G holds a |^ (card G) = 1_ G