theorem Th4: :: FIB_NUM:4

for m, n being Nat holds Fib (m + (n + 1)) = ((Fib n) * (Fib m)) + ((Fib (n + 1)) * (Fib (m + 1)))