let n be Nat; :: thesis: for i being Integer holds
( (scf i) . 0 = i & (scf i) . (n + 1) = 0 )
let i be Integer; :: thesis: ( (scf i) . 0 = i & (scf i) . (n + 1) = 0 )
defpred S2[ Nat] means ( (rfs i) . ($1 + 1) = 0 & (scf i) . ($1 + 1) = 0 );
thus (scf i) . 0 = [\((rfs i) . 0)/] by Def4
.= [\i/] by Def3
.= i ; :: thesis: (scf i) . (n + 1) = 0
A1: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A2: S2[n] ; :: thesis: S2[n + 1]
thus (rfs i) . ((n + 1) + 1) = 1 / (frac ((rfs i) . (n + 1))) by Def3
.= 1 / (0 - 0) by A2
.= 0 ; :: thesis: (scf i) . ((n + 1) + 1) = 0
thus (scf i) . ((n + 1) + 1) = [\((rfs i) . ((n + 1) + 1))/] by Def4
.= [\0/] by Th29
.= 0 ; :: thesis: verum
end;
(scf i) . (0 + 1) = [\((rfs i) . (0 + 1))/] by Def4
.= [\0/] by Th29
.= 0 ;
then A3: S2[ 0 ] by Th29;
for n being Nat holds S2[n] from NAT_1:sch 2(A3, A1);
 hence (scf i) . (n + 1) = 0 ; :: thesis: verum