theorem :: TOPREAL6:10

for r being Real
for i, j being Nat st r <> 0 & j <= i holds
r |^ (i -' j) = (r |^ i) / (r |^ j)