theorem :: NEWTON02:95

for t, u, z being Integer holds ((t + u) - z) |^ 2,((t |^ 2) + (u |^ 2)) + (z |^ 2) are_congruent_mod 2