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