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