theorem Th35: :: FIB_NUM2:35

for n being Nat holds (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n