let X be RealUnitarySpace; :: thesis: for seq being sequence of X st seq is V11() holds
seq is convergent
let seq be sequence of X; :: thesis: ( seq is V11() implies seq is convergent )
assume seq is V11() ; :: thesis: seq is convergent
then consider x being Point of X such that
A1: for n being Nat holds seq . n = x by VALUED_0:def 18;
take g = x; :: according to BHSP_2:def 1 :: thesis: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),g < r
let r be Real; :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),g < r )
assume A2: r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),g < r
take m = 0 ; :: thesis: for n being Element of NAT st n >= m holds
dist (seq . n),g < r
let n be Element of NAT ; :: thesis: ( n >= m implies dist (seq . n),g < r )
assume n >= m ; :: thesis: dist (seq . n),g < r
dist (seq . n),g = dist x,g by A1
.= 0 by BHSP_1:41 ;
hence dist (seq . n),g < r by A2; :: thesis: verum