let a, k be Nat; for n being positive Nat holds (k * ((a |^ n) + 1)) mod a = k mod a
let n be positive Nat; (k * ((a |^ n) + 1)) mod a = k mod a
consider k being Nat such that
A1:
n = 1 + k
by NAT_1:10, NAT_1:14;
a |^ (1 + k) = a * (a |^ k)
by NEWTON:6;
hence
(k * ((a |^ n) + 1)) mod a = k mod a
by A1, Th80; verum