defpred S₁[ Nat] means (3 * (Fib $1)) + (Lucas $1) = 2 * (Fib ($1 + 2));
let n be Nat; :: thesis: (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2))
(0 + 1) + 1 = 2 ;
then A1: Fib 2 = 1 by 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 A3: ( S₁[k] & S₁[k + 1] ) ; :: thesis: S₁[k + 2]
(3 * (Fib (k + 2))) + (Lucas (k + 2)) = (3 * ((Fib k) + (Fib (k + 1)))) + (Lucas (k + 2)) by FIB_NUM2:24
.= ((3 * (Fib k)) + (3 * (Fib (k + 1)))) + ((Lucas k) + (Lucas (k + 1))) by Th12
.= (2 * (Fib (k + 2))) + (2 * (Fib ((k + 1) + 2))) by A3
.= 2 * ((Fib (k + 2)) + (Fib ((k + 2) + 1)))
.= 2 * (Fib ((k + 2) + 2)) by FIB_NUM2:24 ;
hence S₁[k + 2] ; :: thesis: verum

end;

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