let n be Nat; :: thesis: ((Fib n) ^2) + ((Fib (n + 1)) ^2) = Fib ((2 * n) + 1)
defpred S₁[ Nat] means ((Fib $1) ^2) + ((Fib ($1 + 1)) ^2) = Fib ((2 * $1) + 1);
A1: S₁[ 0 ] by PRE_FF:1;
A2: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume A3: S₁[k] ; :: thesis: ( not S₁[k + 1] or S₁[k + 2] )
assume A4: S₁[k + 1] ; :: thesis: S₁[k + 2]
Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4)) by Lm1
.= (Fib ((2 * k) + 3)) + ((Fib ((2 * k) + 3)) + (Fib ((2 * k) + 2))) by Th26
.= ((Fib ((2 * k) + 3)) + (Fib ((2 * k) + 3))) + (Fib ((2 * k) + 2))
.= (2 * (Fib ((2 * k) + 3))) + ((Fib ((2 * k) + 3)) - (Fib ((2 * k) + 1))) by Th28
.= ((2 * ((Fib (k + 1)) ^2)) + (2 * ((Fib (k + 2)) ^2))) + (((Fib (k + 2)) - (Fib k)) * ((Fib (k + 2)) + (Fib k))) by A3, A4
.= ((2 * ((Fib (k + 1)) ^2)) + (2 * ((Fib (k + 2)) ^2))) + ((Fib (k + 1)) * ((Fib (k + 2)) + (Fib k))) by Th29
.= ((Fib (k + 1)) * ((Fib (k + 1)) + ((Fib (k + 1)) + (Fib k)))) + ((Fib (k + 2)) * ((Fib (k + 2)) + ((Fib (k + 2)) + (Fib (k + 1)))))
.= ((Fib (k + 1)) * ((Fib (k + 1)) + (Fib (k + 2)))) + ((Fib (k + 2)) * ((Fib (k + 2)) + ((Fib (k + 2)) + (Fib (k + 1))))) by Th24
.= ((Fib (k + 1)) * ((Fib (k + 2)) + (Fib (k + 1)))) + ((Fib (k + 2)) * ((Fib (k + 2)) + (Fib (k + 3)))) by Th25
.= ((Fib (k + 1)) * (Fib (k + 3))) + (((Fib (k + 2)) * (Fib (k + 2))) + ((Fib (k + 2)) * (Fib (k + 3)))) by Th25
.= ((Fib (k + 3)) * ((Fib (k + 1)) + (Fib (k + 2)))) + ((Fib (k + 2)) ^2)
.= ((Fib (k + 3)) ^2) + ((Fib (k + 2)) ^2) by Th25 ;
hence S₁[k + 2] ; :: thesis: verum

end;

A5: S₁[1] by Th21, PRE_FF:1;
for n being Nat holds S₁[n] from FIB_NUM:sch 1(A1, A5, A2);
hence ((Fib n) ^2) + ((Fib (n + 1)) ^2) = Fib ((2 * n) + 1) ; :: thesis: verum