theorem Th28: :: FIB_NUM3:28

for n being Nat holds Fib (2 * n) = (Fib n) * (Lucas n)