theorem :: NUMBER03:27

for n being Nat
for a, b, k being Integer st a + b > 0 & (a mod k) + (b mod k) > 0 holds
((a + b) to_power n) mod k = (((a mod k) + (b mod k)) to_power n) mod k