theorem Th26: :: PEPIN:26

for n, p being Nat st n <> 0 & p <> 0 holds
n |^ p = n * (n |^ (p -' 1))