theorem Th1: :: FIB_NUM4:1

for a, b being Real
for c being Nat holds (a / b) to_power c = (a to_power c) / (b to_power c)