consider n being natural number such that
A1: ord a = p |^ n by Def1;
ord (a ") = p |^ n by A1, Th5;
hence a " is p -power by Def1; :: thesis: verum