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 ) )

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

( 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 A2:
( ||.seq.|| is convergent & lim ||.seq.|| = 0 )
; :: thesis: ( seq is convergent & lim seq = 0. X )
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;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

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

then
seq is convergent
by NORMSP_1:def 6;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

end;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;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

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