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