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 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 |.||.((S . m) - g).||.| < p by NORMSP_1:def 4;
hence ||.((S . m) - g).|| < r by ABSVALUE:def 1, NORMSP_1:4; :: thesis: verum

end;

hence S is convergent ; :: thesis: lim S = g
hence lim S = g by A2, NORMSP_1:def 7; :: 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