theorem Th77: :: PREPOWER:77

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