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 )

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

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

hence
a * z is non-zero
by Th7; :: thesis: a * z is 0. S -convergent 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;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

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

hence
a * z is convergent
; :: according to NDIFF_1:def 4 :: thesis: lim (a * z) = 0. Sex 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 )

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

then consider pp being Real such that
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;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

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

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