let n be Element of NAT ; :: thesis: Fib ((2 * n) + 1) = ((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n))
((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n)) = (Fib (2 * (n + 1))) - ((Fib n) * (Lucas n)) by Th28
.= (Fib ((2 * n) + 2)) - (Fib (2 * n)) by Th28
.= Fib ((2 * n) + 1) by FIB_NUM2:29 ;
hence Fib ((2 * n) + 1) = ((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n)) ; :: thesis: verum