let i be Integer; :: thesis: i '*' (1. INT.Ring) = i
set R = INT.Ring ;
defpred S₁[ Integer] means for k being Integer st k = $1 holds
k = k '*' (1. INT.Ring);
0 '*' (1. INT.Ring) = 0. INT.Ring by Th58;
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. INT.Ring) by Lm6
.= u - 1 by A3 ;
hence S₁[u - 1] ; :: thesis: S₁[u + 1]
(u + 1) '*' (1. INT.Ring) = (u '*' (1. INT.Ring)) + (1. INT.Ring) by Lm5
.= u + 1 by A3 ;
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