theorem Th2: :: JORDAN1D:2

for i being Nat
for r being Real st r <> 0 holds
(1 / r) * (r |^ (i + 1)) = r |^ i