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