theorem :: PREPOWER:91

for a, b, c being Real st a > 0 holds
(a #R b) #R c = a #R (b * c)