let n be Nat; :: thesis: Fib (2 * n) = (Fib n) * (Lucas n)
A1: n in NAT by ORDINAL1:def 12;
(Fib n) * (Lucas n) = (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (Lucas n) by FIB_NUM:7
.= (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * ((tau to_power n) + (tau_bar to_power n)) by Th21
.= (((tau to_power n) + (tau_bar to_power n)) * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74
.= (((tau to_power n) to_power 2) - ((tau_bar to_power n) to_power 2)) / (sqrt 5) by Th7
.= (((tau to_power n) to_power 2) - (tau_bar to_power (2 * n))) / (sqrt 5) by A1, Th6
.= ((tau to_power (2 * n)) - (tau_bar to_power (2 * n))) / (sqrt 5) by POWER:33
.= Fib (2 * n) by FIB_NUM:7 ;
hence Fib (2 * n) = (Fib n) * (Lucas n) ; :: thesis: verum