theorem :: FIB_NUM2:65

for n being Element of NAT holds Sum (EvenFibs ((2 * n) + 2)) = (Fib ((2 * n) + 3)) - 1