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 )

A1: now

assume that
A2: seq is V8() and
A3: r in rng seq ; :: 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 )
consider r1 being Real such that
A4: rng seq = {r1} by A2, FUNCT_2:188;
consider r2 being Real such that
A5: for n being Nat holds seq . n = r2 by A2, 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 ( ( ( 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 ) by A2, SEQ_2:def 7; :: thesis: verum

end;

A8: now

assume that
A9: seq is V8() and
A10: ex n being Element of NAT st seq . n = r ; :: 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 )
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 ( ( ( 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 ) by A1, A9, A11, FUNCT_1:def 5; :: thesis: verum

end;

assume ( ( 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
hence lim seq = r by A1, A8; :: thesis: verum