theorem Th64: :: FIB_NUM2:64
for n being Nat holds OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*>