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;