theorem :: PREPOWER:80
for a, b, c being Real st a > 0 & b > 0 holds
(a / b) #R c = (a #R c) / (b #R c)