theorem Th81: :: NEWTON02:81

for a, k being Nat
for n being positive Nat holds (k * ((a |^ n) + 1)) mod a = k mod a