theorem Th71: :: CARDFIL4:84

for f being Function of ([#] OrderedNAT),R^1
for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds
lim_f f = {(lim seq)}