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 ; :: 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 ;
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 ;
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 ; :: thesis: verum