theorem :: FIB_NUM3:26

for n, m being Element of NAT holds 2 * (Lucas (n + m)) = ((Lucas n) * (Lucas m)) + ((5 * (Fib n)) * (Fib m))