let r be real number ; :: thesis: for seq being Real_Sequence st ( ( seq is V8() & r in rng seq ) or ( seq is V8() & ex n being Element of NAT st seq . n = r ) ) holds
lim seq = r
let seq be Real_Sequence; :: thesis: ( ( ( seq is V8() & r in rng seq ) or ( seq is V8() & ex n being Element of NAT st seq . n = r ) ) implies lim seq = r )
assume A1: ( ( seq is V8() & r in rng seq ) or ( seq is V8() & ex n being Element of NAT st seq . n = r ) ) ; :: thesis: lim seq = r

A2: now

assume that
A3: seq is V8() and
A4: r in rng seq ; :: thesis: lim seq = r
consider r1 being Real such that
A5: rng seq = {r1} by A3, FUNCT_2:188;
consider r2 being Real such that
A6: for n being Nat holds seq . n = r2 by A3, VALUED_0:def 18;
A7: r = r1 by A4, A5, 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 A9: 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 A6;
then r2 = r by A5, A7, TARSKI:def 1;
then seq . m = r by A6;
hence abs ((seq . m) - r) < p by A9, ABSVALUE:7; :: thesis: verum

end;

hence lim seq = r by A3, SEQ_2:def 7; :: thesis: verum

end;

now

assume that
A10: seq is V8() and
A11: ex n being Element of NAT st seq . n = r ; :: thesis: lim seq = r
consider n being Element of NAT such that
A12: seq . n = r by A11;
n in NAT ;
then n in dom seq by FUNCT_2:def 1;
hence lim seq = r by A2, A10, A12, FUNCT_1:def 5; :: thesis: verum

end;

hence lim seq = r by A1, A2; :: thesis: verum