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

now

let n be Element of NAT ; :: thesis: not (a * z) . n = 0. S
a is non-empty by FDIFF_1:def 1;
then 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; :: according to NDIFF_1:def 4 :: thesis: ( a * z is convergent & lim (a * z) = 0. S )

A3: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p )
assume A4: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of 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 ) by FDIFF_1:def 1;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs ((a . m) - 0) < pp by A7, SEQ_2:def 7;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.(((a * z) . m) - (0. S)).|| < p )
assume n <= m ; :: thesis: ||.(((a * z) . m) - (0. S)).|| < p
then A10: abs ((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
.= (abs (a . m)) * ||.z.|| by NORMSP_1:def 1 ;
0 <= ||.z.|| by NORMSP_1:4;
then (abs (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 by NORMSP_1:def 6; :: thesis: lim (a * z) = 0. S
hence lim (a * z) = 0. S by A3, NORMSP_1:def 7; :: thesis: verum