canHom_Int INT.Ring = id INT.Ring by Th83;
hence for f being Homomorphism of INT.Ring,INT.Ring holds f = id INT.Ring by Th83; :: thesis: verum