theorem Th5: :: FIB_NUM2:5

for k, m being Nat
for a being Real holds a to_power (k + m) = (a to_power k) * (a to_power m)