for G being Group
for a, b being Element of G
for p being prime Nat st a |^ b is p -power holds
a is p -power