let i be Integer; :: thesis: i '*' (1. INT.Ring) = i
set R = INT.Ring ;
defpred S₁[ Integer] means $1 = $1 '*' (1. INT.Ring);
0 '*' (1. INT.Ring) = 0. INT.Ring by RING_3:59;
then A1: S₁[ 0 ] ;

A2: now :: thesis: for u being Integer st S₁[u] holds
( S₁[u - 1] & S₁[u + 1] )

let u be Integer; :: thesis: ( S₁[u] implies ( S₁[u - 1] & S₁[u + 1] ) )
assume A3: S₁[u] ; :: thesis: ( S₁[u - 1] & S₁[u + 1] )
(u - 1) '*' (1. INT.Ring) = (u '*' (1. INT.Ring)) - (1 '*' (1. INT.Ring)) by RING_3:64
.= u - 1 by A3, RING_3:60 ;
hence S₁[u - 1] ; :: thesis: S₁[u + 1]
(u + 1) '*' (1. INT.Ring) = (u '*' (1. INT.Ring)) + (1 '*' (1. INT.Ring)) by RING_3:62
.= u + 1 by A3, RING_3:60 ;
hence S₁[u + 1] ; :: thesis: verum

end;

for k being Integer holds S₁[k] from INT_1:sch 4(A1, A2);
hence i '*' (1. INT.Ring) = i ; :: thesis: verum