theorem Th2: :: FIB_NUM4:2
for a being Real
for b, c being Integer st a <> 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)