theorem Th9: :: FIB_NUM2:9

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