let n be Nat; :: thesis: for k being non zero Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))
defpred S₁[ Nat] means Fib (n + $1) = ((Fib $1) * (Fib (n + 1))) + ((Fib ($1 -' 1)) * (Fib n));
((Fib 1) * (Fib (n + 1))) + ((Fib (1 -' 1)) * (Fib n)) = (1 * (Fib (n + 1))) + (0 * (Fib n)) by PRE_FF:1, XREAL_1:232
.= Fib (n + 1) ;
then A1: S₁[1] ;
A2: for m being non zero Nat st S₁[m] & S₁[m + 1] holds
S₁[m + 2]

proof

let m be non zero Nat; :: thesis: ( S₁[m] & S₁[m + 1] implies S₁[m + 2] )
A3: m >= 1 by NAT_2:19;
set F2 = (Fib (m + 2)) * (Fib (n + 1));
set F1 = (Fib (n + 1)) * (Fib (m + 2));
set k = m -' 1;
assume A4: ( S₁[m] & S₁[m + 1] ) ; :: thesis: S₁[m + 2]
Fib (n + (m + 2)) = Fib ((n + m) + 2)
.= (Fib (n + m)) + (Fib ((n + m) + 1)) by Th24
.= (((Fib m) * (Fib (n + 1))) + ((Fib (m -' 1)) * (Fib n))) + (((Fib (m + 1)) * (Fib (n + 1))) + ((Fib (m + (1 -' 1))) * (Fib n))) by A4, NAT_D:38
.= (((Fib m) * (Fib (n + 1))) + ((Fib (m -' 1)) * (Fib n))) + (((Fib (m + 1)) * (Fib (n + 1))) + ((Fib (m + 0)) * (Fib n))) by XREAL_1:232
.= ((Fib (n + 1)) * ((Fib m) + (Fib (m + 1)))) + ((Fib n) * ((Fib (m -' 1)) + (Fib m)))
.= ((Fib (n + 1)) * (Fib (m + 2))) + ((Fib n) * ((Fib (m -' 1)) + (Fib m))) by Th24
.= ((Fib (n + 1)) * (Fib (m + 2))) + ((Fib n) * ((Fib (m -' 1)) + (Fib ((m -' 1) + 1)))) by A3, XREAL_1:235
.= ((Fib (m + 2)) * (Fib (n + 1))) + ((Fib n) * (Fib ((m -' 1) + 2))) by Th24
.= ((Fib (m + 2)) * (Fib (n + 1))) + ((Fib ((m + 2) -' 1)) * (Fib n)) by A3, NAT_D:38 ;
hence S₁[m + 2] ; :: thesis: verum

end;

2 -' 1 = 2 - 1 by NAT_D:39;
then A5: S₁[2] by Th21, Th24, PRE_FF:1;
for k being non zero Nat holds S₁[k] from FIB_NUM2:sch 1(A1, A5, A2);
hence for k being non zero Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n)) ; :: thesis: verum