defpred S₁[ Nat] means (Lucas ($1 + 3)) - (2 * (Lucas $1)) = 5 * (Fib $1);
A1: S₁[1] by Th11, Th16, PRE_FF:1;
A2: 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
A3: S₁[k] and
A4: S₁[k + 1] ; :: thesis: S₁[k + 2]
(Lucas ((k + 2) + 3)) - (2 * (Lucas (k + 2))) = (Lucas (((((k + 1) + 1) + 1) + 1) + 1)) - (2 * (Lucas (k + 2)))
.= ((Lucas (k + 3)) + (Lucas (k + 4))) - (2 * (Lucas (k + 2))) by Th11 ;
then (Lucas ((k + 2) + 3)) - (2 * (Lucas (k + 2))) = ((Lucas (k + 3)) + (Lucas (k + 4))) - (2 * ((Lucas k) + (Lucas (k + 1)))) by Th12
.= ((Lucas (k + 4)) - (2 * (Lucas (k + 1)))) + (5 * (Fib k)) by A3
.= (5 * (Fib k)) + (5 * (Fib (k + 1))) by A4
.= 5 * ((Fib k) + (Fib (k + 1)))
.= 5 * (Fib ((k + 1) + 1)) by PRE_FF:1
.= 5 * (Fib (k + 2)) ;
hence S₁[k + 2] ; :: thesis: verum

end;

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