theorem :: CARDFIL4:85

for T being non empty TopSpace
for f being Function of ([#] OrderedNAT),T
for s being sequence of T st f = s holds
lim_f f = lim_f s by CARDFIL2:54;