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