theorem :: FIB_NUM3:43

for n, m being Nat holds ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib ((Fib 0),(Lucas 0),(n + m))