theorem :: REAL_3:32

for n being Nat
for i being Integer st i > 1 holds
( (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) by Lm5;