reconsider e = 1 as Element of INT.Ring by INT_1:def 1;
for x being Element of INT.Ring holds
( x * e = x & e * x = x ) ;
then 1_ INT.Ring = e by GROUP_1:def 5;
hence 1_ INT.Ring = 1 ; :: thesis: verum