let G be Group; :: thesis: for a, b being Element of G
for p being natural prime number st a |^ b is p -power holds
a is p -power
let a, b be Element of G; :: thesis: for p being natural prime number st a |^ b is p -power holds
a is p -power
let p be natural prime number ; :: thesis: ( a |^ b is p -power implies a is p -power )
assume a |^ b is p -power ; :: thesis: a is p -power
then consider r being natural number such that
A1: ord (a |^ b) = p |^ r by Def1;
ord a = p |^ r by A1, Th6;
hence a is p -power by Def1; :: thesis: verum