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 * < p )
proof
take pp = p / ( + 1); :: thesis: ( pp > 0 & pp * < p )
A5: ( ||.z.|| + 0 < + 1 & 0 <= ) by ;
A6: ||.z.|| + 1 > 0 + 0 by ;
then 0 < p / ( + 1) by ;
then pp * < pp * ( + 1) by ;
hence ( pp > 0 & pp * < p ) by ; :: thesis: verum
end;
then consider pp being Real such that
A7: pp > 0 and
A8: pp * < 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 ;
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).| * by NORMSP_1:def 1 ;
0 <= by NORMSP_1:4;
then |.(a . m).| * <= pp * by ;
hence ||.(((a * z) . m) - (0. S)).|| < p by ; :: 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 ; :: thesis: verum