theorem Th4: :: IRRAT_1:4

for k, n being Nat st n > 0 holds
n ^ (- (k + 1)) = (n ^ (- k)) / n