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:42;
m |^ 0 = 1 by NEWTON:4;
hence 1_ G is m -power by A1; :: thesis: verum