let a, b be odd Integer; :: thesis: for m being odd Nat holds Parity ((a |^ m) + (b |^ m)) = Parity (a + b)
let m be odd Nat; :: thesis: Parity ((a |^ m) + (b |^ m)) = Parity (a + b)

per cases ( a + b = 0 or a + b <> 0 ) ;

suppose A1: a + b = 0 ; :: thesis: Parity ((a |^ m) + (b |^ m)) = Parity (a + b)

then a = - b ;
then a |^ m = - (b |^ m) by POWER:2;
hence Parity ((a |^ m) + (b |^ m)) = Parity (a + b) by A1; :: thesis: verum

end;

suppose A1: a + b <> 0 ; :: thesis: Parity ((a |^ m) + (b |^ m)) = Parity (a + b)

then a <> - b ;
then a |^ m <> (- b) |^ m by NEWTON03:13;
then a |^ m <> - (b |^ m) by POWER:2;
then (a |^ m) + (b |^ m) <> 0 ;
then ( Parity ((a |^ m) + (b |^ m)) = 2 |^ (2 |-count ((a |^ m) + (b |^ m))) & Parity (a + b) = 2 |^ (2 |-count (a + b)) ) by A1, Def1;
hence Parity ((a |^ m) + (b |^ m)) = Parity (a + b) by NEWTON03:81; :: thesis: verum

end;

end;