let r be real number ; :: thesis: for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Element of 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 Element of NAT st seq . n = r ) implies lim seq = r )
assume Z: seq is constant ; :: thesis: ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r )
then consider r1 being Real such that
A4: rng seq = {r1} by FUNCT_2:188;

A1: now

assume A3: r in rng seq ; :: thesis: ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r )
consider r2 being Real such that
A5: for n being Nat holds seq . n = r2 by Z, VALUED_0:def 18;
A6: r = r1 by A3, A4, TARSKI:def 1;

now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p )
assume A7: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq . m) - r) < p )
assume n <= m ; :: thesis: abs ((seq . m) - r) < p
m in NAT ;
then m in dom seq by FUNCT_2:def 1;
then seq . m in rng seq by FUNCT_1:def 5;
then r2 in rng seq by A5;
then r2 = r by A4, A6, TARSKI:def 1;
then seq . m = r by A5;
hence abs ((seq . m) - r) < p by A7, ABSVALUE:7; :: thesis: verum

end;

hence ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r ) by Z, SEQ_2:def 7; :: thesis: verum

end;

A8: now

assume A10: ex n being Element of NAT st seq . n = r ; :: thesis: ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r )
consider n being Element of NAT such that
A11: seq . n = r by A10;
n in NAT ;
then n in dom seq by FUNCT_2:def 1;
hence ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r ) by A1, A11, FUNCT_1:def 5; :: thesis: verum

end;

assume ( r in rng seq or ex n being Element of NAT st seq . n = r ) ; :: thesis: lim seq = r
hence lim seq = r by A1, A8; :: thesis: verum