theorem Th10: :: FIB_NUM3:10

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