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 )

proof

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;

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

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

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

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;

hence lim seq = g by A1, Def2; :: thesis: verum

end;

hence ( ( 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 ) ; :: thesis: verum