theorem Th5: :: LPSPACE2:5

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