let t, u, z be Integer; :: thesis: ( (u + t) + z is even implies (u * t) * z is even )
assume A1: (u + t) + z is even ; :: thesis: (u * t) * z is even

per cases ( u is even or u is odd ) ;

suppose u is even ; :: thesis: (u * t) * z is even

hence (u * t) * z is even ; :: thesis: verum

end;

suppose B1: u is odd ; :: thesis: (u * t) * z is even

per cases ( t is even or t is odd ) ;

suppose t is even ; :: thesis: (u * t) * z is even

hence (u * t) * z is even ; :: thesis: verum

end;

suppose t is odd ; :: thesis: (u * t) * z is even

then z is even by A1, B1;
hence (u * t) * z is even ; :: thesis: verum

end;

end;

end;

end;