for G being Group
for m being Nat holds 1_ G is m -power