let n be Nat; :: thesis: for t, u being Integer holds t + u divides ((t + (2 * u)) |^ n) - (u |^ n)
let t, u be Integer; :: thesis: t + u divides ((t + (2 * u)) |^ n) - (u |^ n)
t + u divides (((t + u) + u) |^ n) - (u |^ n) by Th10;
hence t + u divides ((t + (2 * u)) |^ n) - (u |^ n) ; :: thesis: verum