for a, b, c, m, l being Nat
for n being positive Nat holds ((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = (b + c) mod a