let G be Group; :: thesis: for m being Nat holds 1_ G is m -power
let m be Nat; :: thesis: 1_ G is m -power
A1: ord (1_ G) = 1 by GROUP_1:84;
m |^ 0 = 1 by NEWTON:9;
hence 1_ G is m -power by A1, Def1; :: thesis: verum