theorem Th89: :: NEWTON02:89

for a, b, c being Nat
for n being odd Nat holds ((a + b) - c) mod 3 = (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3