let X be RealNormSpace; :: thesis: for seq being sequence of X holds
( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) )
thus ( seq is convergent & lim seq = 0. X implies ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) ) :: thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = 0 implies ( seq is convergent & lim seq = 0. X ) )

proof

assume A1: ( seq is convergent & lim seq = 0. X ) ; :: thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = 0 )
then lim ||.seq.|| = ||.(0. X).|| by LOPBAN_1:20;
hence ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) by A1, LOPBAN_1:20, NORMSP_1:1; :: thesis: verum

end;

assume A2: ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) ; :: thesis: ( seq is convergent & lim seq = 0. X )

A3: now :: thesis: for p being Real st 0 < p holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - (0. X)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - (0. X)).|| < p )
assume 0 < p ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - (0. X)).|| < p
then consider m being Nat such that
A4: for n being Nat st m <= n holds
|.((||.seq.|| . n) - 0).| < p by A2, SEQ_2:def 7;
take m = m; :: thesis: for n being Nat st m <= n holds
||.((seq . n) - (0. X)).|| < p

hereby :: thesis: verum

let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - (0. X)).|| < p )
assume m <= n ; :: thesis: ||.((seq . n) - (0. X)).|| < p
then |.((||.seq.|| . n) - 0).| < p by A4;
then A5: |.||.(seq . n).||.| < p by NORMSP_0:def 4;
0 <= ||.(seq . n).|| by NORMSP_1:4;
then ||.(seq . n).|| < p by A5, ABSVALUE:def 1;
hence ||.((seq . n) - (0. X)).|| < p by RLVECT_1:13; :: thesis: verum

end;

end;

then seq is convergent by NORMSP_1:def 6;
hence ( seq is convergent & lim seq = 0. X ) by A3, NORMSP_1:def 7; :: thesis: verum