theorem Th27: :: POWER:27

for a, b, c being Real st a > 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)