theorem Th7: :: FIB_NUM:7

for n being Nat holds Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)