defpred S₁[ Nat] means for n being Element of NAT holds 2 * (Lucas (n + $1)) = ((Lucas n) * (Lucas $1)) + ((5 * (Fib n)) * (Fib $1));

A1: now

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A2: S₁[k] and
A3: S₁[k + 1] ; :: thesis: S₁[k + 2]
thus S₁[k + 2] :: thesis: verum

proof

let n be Element of NAT ; :: thesis: 2 * (Lucas (n + (k + 2))) = ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2)))
A4: 2 * (Lucas (n + (k + 1))) = ((Lucas n) * (Lucas (k + 1))) + ((5 * (Fib n)) * (Fib (k + 1))) by A3;
2 * (Lucas (n + (k + 2))) = 2 * (Lucas ((n + k) + 2))
.= 2 * ((Lucas (n + k)) + (Lucas ((n + k) + 1))) by Th12
.= (2 * (Lucas (n + k))) + (2 * (Lucas ((n + k) + 1)))
.= (((Lucas n) * (Lucas k)) + ((5 * (Fib n)) * (Fib k))) + (2 * (Lucas (n + (k + 1)))) by A2
.= ((Lucas n) * ((Lucas k) + (Lucas (k + 1)))) + ((5 * (Fib n)) * ((Fib k) + (Fib (k + 1)))) by A4
.= ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * ((Fib k) + (Fib (k + 1)))) by Th12
.= ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2))) by FIB_NUM2:26 ;
hence 2 * (Lucas (n + (k + 2))) = ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2))) ; :: thesis: verum

end;

end;

A5: S₁[1]

proof

let n be Element of NAT ; :: thesis: 2 * (Lucas (n + 1)) = ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1))
2 * (Lucas (n + 1)) = (((Lucas (n + 1)) + (Lucas n)) + (Lucas (n + 1))) - (Lucas n)
.= ((Lucas (n + 1)) + (Lucas (n + 2))) - (Lucas n) by Th12
.= (Lucas (n + 3)) - (Lucas n) by Th13
.= (Lucas n) + ((Lucas (n + 3)) - (2 * (Lucas n)))
.= ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1)) by Th11, Th23, PRE_FF:1 ;
hence 2 * (Lucas (n + 1)) = ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1)) ; :: thesis: verum

end;

A6: S₁[ 0 ] by Th11, PRE_FF:1;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A6, A5, A1);
hence for n, m being Element of NAT holds 2 * (Lucas (n + m)) = ((Lucas n) * (Lucas m)) + ((5 * (Fib n)) * (Fib m)) ; :: thesis: verum