theorem :: FIB_NUM3:30

for n being Element of NAT holds (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1))