theorem Th21: :: FIB_NUM3:21

for n being Nat holds Lucas n = (tau to_power n) + (tau_bar to_power n)