theorem Th30: :: REAL_3:30

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