defpred S₁[ Nat] means Fib ($1 + 2) = (Fib $1) + (Fib ($1 + 1));
let n be Nat; :: thesis: Fib (n + 2) = (Fib n) + (Fib (n + 1))
A1: 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 S₁[k] ; :: thesis: ( not S₁[k + 1] or S₁[k + 2] )
assume S₁[k + 1] ; :: thesis: S₁[k + 2]
Fib ((k + 2) + 2) = Fib (((k + 2) + 1) + 1)
.= (Fib (k + 2)) + (Fib ((k + 2) + 1)) by PRE_FF:1 ;
hence S₁[k + 2] ; :: thesis: verum

end;

Fib (0 + 2) = Fib ((0 + 1) + 1)
.= (Fib 0) + (Fib 1) by PRE_FF:1 ;
then A2: S₁[ 0 ] ;
A3: S₁[1] by PRE_FF:1;
for n being Nat holds S₁[n] from FIB_NUM:sch 1(A2, A3, A1);
hence Fib (n + 2) = (Fib n) + (Fib (n + 1)) ; :: thesis: verum