theorem Th8: :: FIB_NUM3:8

for n being Element of NAT
for a, b being non zero Real holds (a * b) to_power n = (a to_power n) * (b to_power n)