theorem Th58: :: NEWTON02:156

for a being Nat
for n being prime Nat holds n divides (a |^ n) - a