defpred S₁[ Nat] means (2 * (Lucas $1)) + (Lucas ($1 + 1)) = 5 * (Fib ($1 + 1));
A1: S₁[ 0 ] by Th11, PRE_FF:1;
A2: S₁[1]

proof

(0 + 1) + 1 = 2 ;
then Fib 2 = 1 by PRE_FF:1;
hence S₁[1] by Th11, Th14; :: thesis: verum

end;

A3: 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 that
A4: S₁[k] and
A5: S₁[k + 1] ; :: thesis: S₁[k + 2]
(2 * (Lucas (k + 2))) + (Lucas ((k + 2) + 1)) = (2 * (Lucas (k + 2))) + (Lucas (k + (2 + 1)))
.= (2 * (Lucas (k + 2))) + ((Lucas (k + 1)) + (Lucas (k + 2))) by Th13
.= ((2 * (Lucas (k + 2))) + (Lucas (k + 1))) + (Lucas (k + 2))
.= ((2 * (Lucas (k + 2))) + (Lucas (k + 1))) + ((Lucas k) + (Lucas (k + 1))) by Th12
.= ((Lucas (k + 2)) + ((2 * (Lucas (k + 1))) + (Lucas (k + 2)))) + (Lucas k)
.= (((Lucas k) + (Lucas (k + 1))) + (5 * (Fib (k + 2)))) + (Lucas k) by A5, Th12
.= (5 * (Fib (k + 1))) + (5 * (Fib (k + 2))) by A4
.= 5 * ((Fib (k + 1)) + (Fib (k + (1 + 1))))
.= 5 * (Fib (((k + 1) + 1) + 1)) by PRE_FF:1
.= 5 * (Fib ((k + 2) + 1)) ;
hence S₁[k + 2] ; :: thesis: verum

end;

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