let f be Function of ([#] OrderedNAT),R^1; :: thesis: for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds

lim_f f = {(lim seq)}

let seq be Function of NAT,REAL; :: 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)}

consider x being object such that

A3: x in lim_f f by A2, XBOOLE_0:def 1;

reconsider y = x as Point of R^1 by A3;

consider u being object such that

A4: lim_f f = {u} by A3, ZFMISC_1:131;

lim_f f = {(lim seq)}

lim_f f = {(lim seq)}

let seq be Function of NAT,REAL; :: 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)}

consider x being object such that

A3: x in lim_f f by A2, XBOOLE_0:def 1;

reconsider y = x as Point of R^1 by A3;

consider u being object such that

A4: lim_f f = {u} by A3, ZFMISC_1:131;

lim_f f = {(lim seq)}

proof

hence
lim_f f = {(lim seq)}
; :: thesis: verum
lim_f f c= {(lim seq)}

end;proof

hence
lim_f f = {(lim seq)}
by A4, ZFMISC_1:3; :: thesis: verum
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in lim_f f or t in {(lim seq)} )

assume A5: t in lim_f f ; :: thesis: t in {(lim seq)}

then reconsider t1 = t as Real ;

A6: ( seq is convergent & ex z being Real st

( z in lim_f f & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - z).| < p ) ) ) by A1, A2, Th70;

consider z being Real such that

A7: z in lim_f f and

A8: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - z).| < p by A1, A2, Th70;

( t = u & z = u ) by A5, A7, A4, TARSKI:def 1;

then t1 = lim seq by A8, A6, SEQ_2:def 7;

hence t in {(lim seq)} by TARSKI:def 1; :: thesis: verum

end;assume A5: t in lim_f f ; :: thesis: t in {(lim seq)}

then reconsider t1 = t as Real ;

A6: ( seq is convergent & ex z being Real st

( z in lim_f f & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - z).| < p ) ) ) by A1, A2, Th70;

consider z being Real such that

A7: z in lim_f f and

A8: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - z).| < p by A1, A2, Th70;

( t = u & z = u ) by A5, A7, A4, TARSKI:def 1;

then t1 = lim seq by A8, A6, SEQ_2:def 7;

hence t in {(lim seq)} by TARSKI:def 1; :: thesis: verum