theorem Th75: :: PREPOWER:75

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