let x be Element of INT.Ring ; :: according to VECTSP_1:def 16 :: thesis: ( x * (1. INT.Ring ) = x & (1. INT.Ring ) * x = x )
1 in INT by INT_1:def 2;
then 1 = 1. INT.Ring by FUNCT_7:def 1;
hence ( x * (1. INT.Ring ) = x & (1. INT.Ring ) * x = x ) ; :: thesis: verum