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

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. F_Rat) = (u '*' (1. F_Rat)) - (1 '*' (1. F_Rat)) by RING_3:64
.= u - 1 by A3, GAUSSINT:def 14, RING_3:60 ;
hence S₁[u - 1] ; :: thesis: S₁[u + 1]
(u + 1) '*' (1. F_Rat) = (u '*' (1. F_Rat)) + (1 '*' (1. F_Rat)) by RING_3:62
.= u + 1 by A3, GAUSSINT:def 14, 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. F_Rat) = i ; :: thesis: verum