let a, n, k be Nat; :: thesis: for b being non zero Nat holds ((a mod (b |^ (n + k))) - (a mod (b |^ n))) mod (b |^ n) = 0
let b be non zero Nat; :: thesis: ((a mod (b |^ (n + k))) - (a mod (b |^ n))) mod (b |^ n) = 0
b |^ n divides (a mod (b |^ (n + k))) - (a mod (b |^ n)) by DAS;
hence ((a mod (b |^ (n + k))) - (a mod (b |^ n))) mod (b |^ n) = 0 ; :: thesis: verum