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

assume A1: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ; :: thesis: ( S is convergent & lim S = g )

A2: now

let r be Real; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r )
reconsider p = r as real number ;
assume 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
abs ((||.(S - g).|| . m) - 0 ) < p by A1, SEQ_2:def 7;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r

now

let m be Element of NAT ; :: thesis: ( n <= m implies ||.((S . m) - g).|| < p )
assume n <= m ; :: thesis: ||.((S . m) - g).|| < p
then abs ((||.(S - g).|| . m) - 0 ) < p by A3;
then abs ||.((S - g) . m).|| < p by NORMSP_0:def 4;
then A4: abs ||.((S . m) - g).|| < p by NORMSP_1:def 7;
0 <= ||.((S . m) - g).|| by NORMSP_1:8;
hence ||.((S . m) - g).|| < p by A4, ABSVALUE:def 1; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
||.((S . m) - g).|| < r ; :: thesis: verum

end;

hence S is convergent by NORMSP_1:def 9; :: thesis: lim S = g
hence lim S = g by A2, NORMSP_1:def 11; :: thesis: verum

end;

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