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)}
proof
lim_f f c= {(lim seq)}
proof
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;
hence lim_f f = {(lim seq)} by A4, ZFMISC_1:3; :: thesis: verum
end;
hence lim_f f = {(lim seq)} ; :: thesis: verum