theorem Th29: :: REAL_3:29

for n being Nat
for i being Integer holds (rfs i) . (n + 1) = 0