theorem Th10: :: FIB_NUM2:10

for k being Nat
for a being non zero Real holds (a to_power k) * (a to_power (- k)) = 1