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