theorem :: FIB_NUM2:39

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