theorem Th13: :: GROUPP_1:13

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