theorem Th9: :: FIB_NUM3:9

for n being Nat holds (tau to_power n) + (tau to_power (n + 1)) = tau to_power (n + 2)