theorem Th7: :: FIB_NUM2:7

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