theorem Th3: :: FIB_NUM2:3

for n being even Integer holds (- 1) to_power n = 1