defpred S₁[ Nat] means Lucas ($1 + 1) = (Fib $1) + (Fib ($1 + 2));
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 A2: ( S₁[k] & S₁[k + 1] ) ; :: thesis: S₁[k + 2]
Fib ((k + 2) + 2) = Fib (((k + 2) + 1) + 1) ;
then A3: Fib ((k + 2) + 2) = (Fib (k + 2)) + (Fib ((k + 2) + 1)) by PRE_FF:1;
Lucas ((k + 2) + 1) = (Lucas (k + 1)) + (Lucas ((k + 1) + 1)) by Th11
.= (((Fib k) + (Fib (k + 1))) + (Fib (k + 2))) + (Fib ((k + 1) + 2)) by A2
.= ((Fib ((k + 1) + 1)) + (Fib (k + 2))) + (Fib ((k + 1) + 2)) by PRE_FF:1
.= (Fib (k + 2)) + (Fib ((k + 2) + 2)) by A3 ;
hence S₁[k + 2] ; :: thesis: verum

end;

(0 + 1) + 1 = 2 ;
then Fib 2 = 1 by PRE_FF:1;
then A4: S₁[1] by Th14, PRE_FF:1;
(0 + 1) + 1 = 2 ;
then A5: S₁[ 0 ] by Th11, PRE_FF:1;
thus for k being Nat holds S₁[k] from FIB_NUM:sch 1(A5, A4, A1); :: thesis: verum