let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds

( seq is convergent iff ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r )

let seq be sequence of X; :: thesis: ( seq is convergent iff ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r )

thus ( seq is convergent implies ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ) :: thesis: ( ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r implies seq is convergent )

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r implies seq is convergent )

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r implies seq is convergent ) ; :: thesis: verum

( seq is convergent iff ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r )

let seq be sequence of X; :: thesis: ( seq is convergent iff ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r )

thus ( seq is convergent implies ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ) :: thesis: ( ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r implies seq is convergent )

proof

( ex g being Point of X st
assume
seq is convergent
; :: thesis: ex g being Point of X st

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r

then consider g being Point of X such that

A1: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r ;

take g ; :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r

then consider m1 being Nat such that

A2: for n being Nat st n >= m1 holds

dist ((seq . n),g) < r by A1;

take k = m1; :: thesis: for n being Nat st n >= k holds

||.((seq . n) - g).|| < r

let n be Nat; :: thesis: ( n >= k implies ||.((seq . n) - g).|| < r )

assume n >= k ; :: thesis: ||.((seq . n) - g).|| < r

then dist ((seq . n),g) < r by A2;

hence ||.((seq . n) - g).|| < r by BHSP_1:def 5; :: thesis: verum

end;for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r

then consider g being Point of X such that

A1: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r ;

take g ; :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r

then consider m1 being Nat such that

A2: for n being Nat st n >= m1 holds

dist ((seq . n),g) < r by A1;

take k = m1; :: thesis: for n being Nat st n >= k holds

||.((seq . n) - g).|| < r

let n be Nat; :: thesis: ( n >= k implies ||.((seq . n) - g).|| < r )

assume n >= k ; :: thesis: ||.((seq . n) - g).|| < r

then dist ((seq . n),g) < r by A2;

hence ||.((seq . n) - g).|| < r by BHSP_1:def 5; :: thesis: verum

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r implies seq is convergent )

proof

hence
( ex g being Point of X st
given g being Point of X such that A3:
for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ; :: thesis: seq is convergent

take g ; :: according to BHSP_2:def 1 :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

then consider m1 being Nat such that

A4: for n being Nat st n >= m1 holds

||.((seq . n) - g).|| < r by A3;

take k = m1; :: thesis: for n being Nat st n >= k holds

dist ((seq . n),g) < r

let n be Nat; :: thesis: ( n >= k implies dist ((seq . n),g) < r )

assume n >= k ; :: thesis: dist ((seq . n),g) < r

then ||.((seq . n) - g).|| < r by A4;

hence dist ((seq . n),g) < r by BHSP_1:def 5; :: thesis: verum

end;ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ; :: thesis: seq is convergent

take g ; :: according to BHSP_2:def 1 :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

then consider m1 being Nat such that

A4: for n being Nat st n >= m1 holds

||.((seq . n) - g).|| < r by A3;

take k = m1; :: thesis: for n being Nat st n >= k holds

dist ((seq . n),g) < r

let n be Nat; :: thesis: ( n >= k implies dist ((seq . n),g) < r )

assume n >= k ; :: thesis: dist ((seq . n),g) < r

then ||.((seq . n) - g).|| < r by A4;

hence dist ((seq . n),g) < r by BHSP_1:def 5; :: thesis: verum

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r implies seq is convergent ) ; :: thesis: verum