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;

A2: now

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A3: S₁[k] and
A4: S₁[k + 1] ; :: thesis: S₁[k + 2]
thus S₁[k + 2] :: thesis: verum

proof

let n be Nat; :: thesis: Fib ((k + 2) + (n + 1)) = ((Fib n) * (Fib (k + 2))) + ((Fib (n + 1)) * (Fib ((k + 2) + 1)))
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: verum

end;

end;

A9: S₁[1] by Lm1, PRE_FF:1;
thus for k being Nat holds S₁[k] from FIB_NUM:sch 1(A1, A9, A2); :: thesis: verum