let n be non empty Element of NAT ; :: thesis: ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2 ) = (- 1) |^ n
set a = n -' 1;
A1: n >= 1 by NAT_2:21;
then n = (n -' 1) + 1 by XREAL_1:237;
then ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2 ) = ((Fib (n -' 1)) * (Fib ((n -' 1) + 2))) - ((Fib ((n -' 1) + 1)) ^2 )
.= (- 1) |^ ((n -' 1) + 1) by Th33
.= (- 1) |^ n by A1, XREAL_1:237 ;
hence ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2 ) = (- 1) |^ n ; :: thesis: verum