let G be Group; :: thesis: for a, b being Element of G
for p being prime Nat st a |^ b is p -power holds
a is p -power
let a, b be Element of G; :: thesis: for p being prime Nat st a |^ b is p -power holds
a is p -power
let p be prime Nat; :: 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 Nat such that
A1: ord (a |^ b) = p |^ r ;
ord a = p |^ r by A1, Th6;
hence a is p -power ; :: thesis: verum