let r be Real; :: thesis: for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Nat st seq . n = r ) holds
lim seq = r
let seq be Real_Sequence; :: thesis: ( seq is constant & ( r in rng seq or ex n being Nat st seq . n = r ) implies lim seq = r )
assume A1: seq is constant ; :: thesis: ( ( not r in rng seq & ( for n being Nat holds not seq . n = r ) ) or lim seq = r )
then consider r1 being Element of REAL such that
A2: rng seq = {r1} by FUNCT_2:111;
A3: now :: thesis: ( r in rng seq & ( r in rng seq or ex n being Nat st seq . n = r ) implies lim seq = r )
assume A4: r in rng seq ; :: thesis: ( ( not r in rng seq & ( for n being Nat holds not seq . n = r ) ) or lim seq = r )
consider r2 being Element of REAL such that
A5: for n being Nat holds seq . n = r2 by A1, VALUED_0:def 18;
A6: r = r1 by A4, A2, TARSKI:def 1;
reconsider zz = 0 as Nat ;
now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < p )
assume A7: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < p
take n = zz; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - r).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - r).| < p )
assume n <= m ; :: thesis: |.((seq . m) - r).| < p
m in NAT by ORDINAL1:def 12;
then m in dom seq by FUNCT_2:def 1;
then seq . m in rng seq by FUNCT_1:def 3;
then r2 in rng seq by A5;
then r2 = r by A2, A6, TARSKI:def 1;
then seq . m = r by A5;
hence |.((seq . m) - r).| < p by A7, ABSVALUE:2; :: thesis: verum
end;
hence ( ( not r in rng seq & ( for n being Nat holds not seq . n = r ) ) or lim seq = r ) by A1, SEQ_2:def 7; :: thesis: verum
end;
A8: now :: thesis: ( ex n being Nat st seq . n = r & ( r in rng seq or ex n being Nat st seq . n = r ) implies lim seq = r )
assume A9: ex n being Nat st seq . n = r ; :: thesis: ( ( not r in rng seq & ( for n being Nat holds not seq . n = r ) ) or lim seq = r )
consider n being Nat such that
A10: seq . n = r by A9;
n in NAT by ORDINAL1:def 12;
then n in dom seq by FUNCT_2:def 1;
hence ( ( not r in rng seq & ( for n being Nat holds not seq . n = r ) ) or lim seq = r ) by A3, A10, FUNCT_1:def 3; :: thesis: verum
end;
assume ( r in rng seq or ex n being Nat st seq . n = r ) ; :: thesis: lim seq = r
hence lim seq = r by A3, A8; :: thesis: verum