let S be RealNormSpace; :: thesis: for a being non-zero 0 -convergent Real_Sequence
for z being Point of S st z <> 0. S holds
( a * z is non-zero & a * z is 0. S -convergent )
let a be non-zero 0 -convergent Real_Sequence; :: thesis: for z being Point of S st z <> 0. S holds
( a * z is non-zero & a * z is 0. S -convergent )
let z be Point of S; :: thesis: ( z <> 0. S implies ( a * z is non-zero & a * z is 0. S -convergent ) )
assume A1: z <> 0. S ; :: thesis: ( a * z is non-zero & a * z is 0. S -convergent )

now :: thesis: for n being Nat holds not (a * z) . n = 0. S

let n be Nat; :: thesis: not (a * z) . n = 0. S
A2: a . n <> 0 by SEQ_1:5;
assume (a * z) . n = 0. S ; :: thesis: contradiction
then (a . n) * z = 0. S by Def3;
hence contradiction by A1, A2, RLVECT_1:11; :: thesis: verum

end;

hence a * z is non-zero by Th7; :: thesis: a * z is 0. S -convergent

A3: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p )
assume A4: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p
ex pp being Real st
( pp > 0 & pp * ||.z.|| < p )

proof

take pp = p / (||.z.|| + 1); :: thesis: ( pp > 0 & pp * ||.z.|| < p )
A5: ( ||.z.|| + 0 < ||.z.|| + 1 & 0 <= ||.z.|| ) by NORMSP_1:4, XREAL_1:8;
A6: ||.z.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.z.|| + 1) by A4, XREAL_1:139;
then pp * ||.z.|| < pp * (||.z.|| + 1) by A5, XREAL_1:97;
hence ( pp > 0 & pp * ||.z.|| < p ) by A4, A6, XCMPLX_1:87; :: thesis: verum

end;

then consider pp being Real such that
A7: pp > 0 and
A8: pp * ||.z.|| < p ;
( a is convergent & lim a = 0 ) ;
then consider n being Nat such that
A9: for m being Nat st n <= m holds
|.((a . m) - 0).| < pp by A7, SEQ_2:def 7;
reconsider n = n as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p
let m be Nat; :: thesis: ( n <= m implies ||.(((a * z) . m) - (0. S)).|| < p )
assume n <= m ; :: thesis: ||.(((a * z) . m) - (0. S)).|| < p
then A10: |.((a . m) - 0).| < pp by A9;
A11: ||.(((a * z) . m) - (0. S)).|| = ||.(((a . m) * z) - (0. S)).|| by Def3
.= ||.((a . m) * z).|| by RLVECT_1:13
.= |.(a . m).| * ||.z.|| by NORMSP_1:def 1 ;
0 <= ||.z.|| by NORMSP_1:4;
then |.(a . m).| * ||.z.|| <= pp * ||.z.|| by A10, XREAL_1:64;
hence ||.(((a * z) . m) - (0. S)).|| < p by A8, A11, XXREAL_0:2; :: thesis: verum

end;

hence a * z is convergent ; :: according to NDIFF_1:def 4 :: thesis: lim (a * z) = 0. S
hence lim (a * z) = 0. S by A3, NORMSP_1:def 7; :: thesis: verum