for a being Element of NAT
for q being Real st 1 < q & q |^ a = 1 holds
a = 0