theorem Th70: :: CARDFIL4:83

for f being Function of ([#] OrderedNAT),R^1
for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds
( seq is convergent & ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) )