let X be RealUnitarySpace; :: thesis: for g being Point of X

for seq being sequence of X st seq is convergent holds

( lim seq = g iff 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 g be Point of X; :: thesis: for seq being sequence of X st seq is convergent holds

( lim seq = g iff 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 implies ( lim seq = g iff 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 ) )

assume A1: seq is convergent ; :: thesis: ( lim seq = g iff 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 ( lim seq = g implies 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: ( ( 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 lim seq = g )

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ) implies lim seq = g )

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ) implies lim seq = g ) ; :: thesis: verum

for seq being sequence of X st seq is convergent holds

( lim seq = g iff 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 g be Point of X; :: thesis: for seq being sequence of X st seq is convergent holds

( lim seq = g iff 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 implies ( lim seq = g iff 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 ) )

assume A1: seq is convergent ; :: thesis: ( lim seq = g iff 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 ( lim seq = g implies 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: ( ( 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 lim seq = g )

proof

( ( for r being Real st r > 0 holds
assume A2:
lim seq = 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

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

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

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 A3;

hence ||.((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

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

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

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

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 A3;

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

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ) implies lim seq = g )

proof

hence
( ( for r being Real st r > 0 holds
assume A4:
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: lim seq = g

end;ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ; :: thesis: lim seq = g

now :: thesis: for r being Real st r > 0 holds

ex k being Nat st

for n being Nat st n >= k holds

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

hence
lim seq = g
by A1, Def2; :: thesis: verumex k being Nat st

for n being Nat st n >= k holds

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

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

for n being Nat st n >= k holds

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

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

for n being Nat st n >= k holds

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

then consider m1 being Nat such that

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

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

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 A5;

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

end;for n being Nat st n >= k holds

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

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

for n being Nat st n >= k holds

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

then consider m1 being Nat such that

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

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

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 A5;

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

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - g).|| < r ) implies lim seq = g ) ; :: thesis: verum