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