let t, u, z be Integer; :: thesis: ((t + u) - z) |^ 2,((t |^ 2) + (u |^ 2)) + (z |^ 2) are_congruent_mod 2
((t - z) + u) |^ 2 = (((((t |^ 2) + (z |^ 2)) + (u |^ 2)) - ((2 * t) * z)) + ((2 * t) * u)) - ((2 * z) * u) by SERIES_4:3;
then (((t - z) + u) |^ 2) - (((t |^ 2) + (z |^ 2)) + (u |^ 2)) = 2 * (((t * u) - (t * z)) - (z * u)) ;
hence ((t + u) - z) |^ 2,((t |^ 2) + (u |^ 2)) + (z |^ 2) are_congruent_mod 2 ; :: thesis: verum