let i be Integer; :: thesis: i '*' (1. F_Rat) = i
set R = F_Rat ;
defpred S1[ Integer] means $1 = $1 '*' (1. F_Rat);
0 '*' (1. F_Rat) = 0. F_Rat by RING_3:59;
then A1: S1[ 0 ] by GAUSSINT:def 14;
A2: now :: thesis: for u being Integer st S1[u] holds
( S1[u - 1] & S1[u + 1] )
let u be Integer; :: thesis: ( S1[u] implies ( S1[u - 1] & S1[u + 1] ) )
assume A3: S1[u] ; :: thesis: ( S1[u - 1] & S1[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 S1[u - 1] ; :: thesis: S1[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 S1[u + 1] ; :: thesis: verum
end;
for k being Integer holds S1[k] from INT_1:sch 4(A1, A2);
 hence i '*' (1. F_Rat) = i ; :: thesis: verum