let n be Nat; :: thesis: for u, v being Integer st n > 0 & u - v is odd holds
( u + v is odd & (u |^ n) - (v |^ n) is odd & (u |^ n) + (v |^ n) is odd )
let u, v be Integer; :: thesis: ( n > 0 & u - v is odd implies ( u + v is odd & (u |^ n) - (v |^ n) is odd & (u |^ n) + (v |^ n) is odd ) )
( ( u is odd or u is even ) & ( v is odd or v is even ) ) ;
hence ( n > 0 & u - v is odd implies ( u + v is odd & (u |^ n) - (v |^ n) is odd & (u |^ n) + (v |^ n) is odd ) ) ; :: thesis: verum