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 )
thus (scf i) . 0 = [\((rfs i) . 0 )/] by Def5
.= [\i/] by Def4
.= i by INT_1:47 ; :: thesis: (scf i) . (n + 1) = 0
defpred S₂[ Nat] means ( (rfs i) . ($1 + 1) = 0 & (scf i) . ($1 + 1) = 0 );
A1: S₂[ 0 ]

proof

thus (rfs i) . (0 + 1) = 0 by Th29; :: thesis: (scf i) . (0 + 1) = 0
thus (scf i) . (0 + 1) = [\((rfs i) . (0 + 1))/] by Def5
.= [\0 /] by Th29
.= 0 ; :: thesis: verum

end;

A2: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A3: S₂[n] ; :: thesis: S₂[n + 1]
thus (rfs i) . ((n + 1) + 1) = 1 / (frac ((rfs i) . (n + 1))) by Def4
.= 1 / (0 - 0 ) by A3
.= 0 ; :: thesis: (scf i) . ((n + 1) + 1) = 0
thus (scf i) . ((n + 1) + 1) = [\((rfs i) . ((n + 1) + 1))/] by Def5
.= [\0 /] by Th29
.= 0 ; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A1, A2);
hence (scf i) . (n + 1) = 0 ; :: thesis: verum