let RNS be RealNormSpace; :: thesis: for S being sequence of RNS

for g being Point of RNS holds

( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )

let S be sequence of RNS; :: thesis: for g being Point of RNS holds

( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )

let g be Point of RNS; :: thesis: ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )

for g being Point of RNS holds

( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )

let S be sequence of RNS; :: thesis: for g being Point of RNS holds

( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )

let g be Point of RNS; :: thesis: ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )

now :: thesis: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 implies ( S is convergent & lim S = g ) )

hence
( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
by NORMSP_1:24; :: thesis: verumassume A1:
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
; :: thesis: ( S is convergent & lim S = g )

hence lim S = g by A2, NORMSP_1:def 7; :: thesis: verum

end;A2: now :: thesis: for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

||.((S . m) - g).|| < r

hence
S is convergent
; :: thesis: lim S = gex n being Nat st

for m being Nat st n <= m holds

||.((S . m) - g).|| < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st

for m being Nat st n <= m holds

||.((S . m) - g).|| < r )

reconsider p = r as Real ;

assume 0 < r ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((S . m) - g).|| < r

then consider n being Nat such that

A3: for m being Nat st n <= m holds

|.((||.(S - g).|| . m) - 0).| < p by A1, SEQ_2:def 7;

reconsider n = n as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

||.((S . m) - g).|| < r

let m be Nat; :: thesis: ( n <= m implies ||.((S . m) - g).|| < r )

assume n <= m ; :: thesis: ||.((S . m) - g).|| < r

then |.((||.(S - g).|| . m) - 0).| < p by A3;

then |.||.((S - g) . m).||.| < p by NORMSP_0:def 4;

then A4: |.||.((S . m) - g).||.| < p by NORMSP_1:def 4;

0 <= ||.((S . m) - g).|| by NORMSP_1:4;

hence ||.((S . m) - g).|| < r by A4, ABSVALUE:def 1; :: thesis: verum

end;for m being Nat st n <= m holds

||.((S . m) - g).|| < r )

reconsider p = r as Real ;

assume 0 < r ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((S . m) - g).|| < r

then consider n being Nat such that

A3: for m being Nat st n <= m holds

|.((||.(S - g).|| . m) - 0).| < p by A1, SEQ_2:def 7;

reconsider n = n as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

||.((S . m) - g).|| < r

let m be Nat; :: thesis: ( n <= m implies ||.((S . m) - g).|| < r )

assume n <= m ; :: thesis: ||.((S . m) - g).|| < r

then |.((||.(S - g).|| . m) - 0).| < p by A3;

then |.||.((S - g) . m).||.| < p by NORMSP_0:def 4;

then A4: |.||.((S . m) - g).||.| < p by NORMSP_1:def 4;

0 <= ||.((S . m) - g).|| by NORMSP_1:4;

hence ||.((S . m) - g).|| < r by A4, ABSVALUE:def 1; :: thesis: verum

hence lim S = g by A2, NORMSP_1:def 7; :: thesis: verum