theorem :: FIB_NUM2:32

for n being non zero Element of NAT holds ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = (- 1) |^ n