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 ) )
now :: thesis: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 implies ( S is convergent & lim S = g ) )
assume A1: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ; :: thesis: ( S is convergent & lim S = g )
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
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 ;
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 ; :: thesis: verum
end;
hence S is convergent ; :: thesis: lim S = g
hence lim S = g by ; :: thesis: verum
end;
hence ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ) by NORMSP_1:24; :: thesis: verum