let seq be Function of NAT,REAL; :: thesis: for f being Function of NAT,R^1 st f = seq & lim_f f <> {} holds
lim_f f = {(lim seq)}
let f be Function of NAT,R^1; :: thesis: ( f = seq & lim_f f <> {} implies lim_f f = {(lim seq)} )
assume that
A1: f = seq and
A2: lim_f f <> {} ; :: thesis: lim_f f = {(lim seq)}
( [#] OrderedNAT = NAT & the carrier of R^1 = REAL ) by STRUCT_0:def 3;
then reconsider f1 = f as Function of ([#] OrderedNAT),R^1 ;
lim_f f = lim_f f1 by CARDFIL2:54;
hence lim_f f = {(lim seq)} by A1, A2, Th71; :: thesis: verum