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