for a being Real
for m, n being Nat st a <> 0 holds
a #Z (m - n) = (a |^ m) / (a |^ n)