theorem Th72: :: CARDFIL4:87

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