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 ( seq is convergent & lim seq = 0. X ) ; :: thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = 0 )
then ( ||.seq.|| is convergent & lim ||.seq.|| = ||.(0. X).|| ) by LOPBAN_1:24;
hence ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) by NORMSP_1:5; :: thesis: verum

end;

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

A2: now

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

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( m <= n implies ||.((seq . n) - (0. X)).|| < p )
assume m <= n ; :: thesis: ||.((seq . n) - (0. X)).|| < p
then abs ((||.seq.|| . n) - 0 ) < p by A3;
then A4: abs ||.(seq . n).|| < p by NORMSP_1:def 10;
0 <= ||.(seq . n).|| by NORMSP_1:8;
then ||.(seq . n).|| < p by A4, ABSVALUE:def 1;
hence ||.((seq . n) - (0. X)).|| < p by RLVECT_1:26; :: thesis: verum

end;

end;

then seq is convergent by NORMSP_1:def 9;
hence ( seq is convergent & lim seq = 0. X ) by A2, NORMSP_1:def 11; :: thesis: verum