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

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