theorem :: FIB_NUM2:66

for n being Nat holds Sum (OddFibs ((2 * n) + 1)) = Fib ((2 * n) + 2)