defpred S₁[ Nat] means for n being Nat holds Fib ($1 + (n + 1)) = ((Fib n) * (Fib $1)) + ((Fib (n + 1)) * (Fib ($1 + 1)));
A1: S₁[ 0 ] by PRE_FF:1;

let n be Nat; :: thesis:
A5: Fib (((k + 1) + 1) + (n + 1)) = Fib (((k + (n + 1)) + 1) + 1)
.= (Fib (k + (n + 1))) + (Fib ((k + 1) + (n + 1))) by PRE_FF:1 ;
set a = (Fib n) * (Fib k);
set b = (Fib (n + 1)) * (Fib (k + 1));
set c = (Fib n) * (Fib (k + 1));
set d = (Fib (n + 1)) * (Fib ((k + 1) + 1));
A6: (((Fib n) * (Fib k)) + ((Fib (n + 1)) * (Fib (k + 1)))) + (((Fib n) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1)))) = (((Fib n) * (Fib k)) + ((Fib n) * (Fib (k + 1)))) + (((Fib (n + 1)) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1)))) ;
A7: ((Fib (n + 1)) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1))) = (Fib (n + 1)) * ((Fib (k + 1)) + (Fib ((k + 1) + 1)))
.= (Fib (n + 1)) * (Fib (((k + 1) + 1) + 1)) by PRE_FF:1 ;
A8: ((Fib n) * (Fib k)) + ((Fib n) * (Fib (k + 1))) = (Fib n) * ((Fib k) + (Fib (k + 1)))
.= (Fib n) * (Fib ((k + 1) + 1)) by PRE_FF:1 ;
Fib (k + (n + 1)) = ((Fib n) * (Fib k)) + ((Fib (n + 1)) * (Fib (k + 1))) by A3;
hence Fib ((k + 2) + (n + 1)) = ((Fib n) * (Fib (k + 2))) + ((Fib (n + 1)) * (Fib ((k + 2) + 1))) by A4, A5, A6, A8, A7; :: thesis:

end;