theorem SC1: :: NEWTON03:48
for a, b being odd Nat
for m being even Nat holds 2 |-count ((a |^ m) + (b |^ m)) = 1