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
thus a * z is non-zero :: according to NDIFF_1:def 4 :: thesis: ( a * z is convergent & lim (a * z) = 0. S )

proof

now

let n be Element of NAT ; :: thesis: not (a * z) . n = 0. S
assume (a * z) . n = 0. S ; :: thesis: contradiction
then A2: (a . n) * z = 0. S by Def3;
a is non-zero by FDIFF_1:def 1;
then ( a . n <> 0 & z <> 0. S ) by A1, SEQ_1:7;
hence contradiction by A2, RLVECT_1:24; :: thesis: verum

end;

hence a * z is non-zero by Th7; :: thesis: verum

end;

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.|| + 1 > 0 + 0 by NORMSP_1:8, XREAL_1:10;
then A6: 0 < p / (||.z.|| + 1) by A4, XREAL_1:141;
A7: ||.z.|| + 0 < ||.z.|| + 1 by XREAL_1:10;
0 <= ||.z.|| by NORMSP_1:8;
then pp * ||.z.|| < pp * (||.z.|| + 1) by A6, A7, XREAL_1:99;
hence ( pp > 0 & pp * ||.z.|| < p ) by A4, A5, XCMPLX_1:88; :: thesis: verum

end;

then consider pp being Real such that
A8: ( pp > 0 & 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 A8, 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 A10: n <= m ; :: thesis: ||.(((a * z) . m) - (0. S)).|| < p
A11: abs ((a . m) - 0 ) < pp by A9, A10;
A12: ||.(((a * z) . m) - (0. S)).|| = ||.(((a . m) * z) - (0. S)).|| by Def3
.= ||.((a . m) * z).|| by RLVECT_1:26
.= (abs (a . m)) * ||.z.|| by NORMSP_1:def 2 ;
0 <= ||.z.|| by NORMSP_1:8;
then (abs (a . m)) * ||.z.|| <= pp * ||.z.|| by A11, XREAL_1:66;
hence ||.(((a * z) . m) - (0. S)).|| < p by A8, A12, XXREAL_0:2; :: thesis: verum

end;

hence a * z is convergent by NORMSP_1:def 9; :: thesis: lim (a * z) = 0. S
hence lim (a * z) = 0. S by A3, NORMSP_1:def 11; :: thesis: verum