let n be non zero 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:19;
then n = (n -' 1) + 1 by XREAL_1:235;
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 Th31
.= (- 1) |^ n by A1, XREAL_1:235 ;
hence ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2) = (- 1) |^ n ; :: thesis: verum