theorem :: CARDFIL4:86

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