theorem Th4: :: FIB_NUM2:4

for m being non zero Real
for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)