let seq be Real_Sequence; :: thesis: ( seq is V8() implies seq is convergent )
assume seq is V8() ; :: thesis: seq is convergent
then consider r being Real such that
A1: for n being Nat holds seq . n = r by VALUED_0:def 18;
take g = r; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((seq . b₃) - g) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq . b₂) - g) ) )
assume A2: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq . b₂) - g) )
take n = 0 ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= abs ((seq . b₁) - g) )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= abs ((seq . m) - g) )
assume n <= m ; :: thesis: not p <= abs ((seq . m) - g)
abs ((seq . m) - g) = abs (r - g) by A1
.= 0 by ABSVALUE:7 ;
hence not p <= abs ((seq . m) - g) by A2; :: thesis: verum