let a be Real; :: thesis: for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
a * S is convergent
let RNS be RealNormSpace; :: thesis: for S being sequence of RNS st S is convergent holds
a * S is convergent
let S be sequence of RNS; :: thesis: ( S is convergent implies a * S is convergent )
assume S is convergent ; :: thesis: a * S is convergent
then consider g being Point of RNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def9;
take h = a * g; :: according to NORMSP_1:def 9 :: thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((a * S) . n) - h).|| < r

A2: now

A3: 0 / (abs a) = 0 ;
assume A4: a <> 0 ; :: thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
then A5: 0 < abs a by COMPLEX1:133;
let r be Real; :: thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume 0 < r ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
then consider m1 being Element of NAT such that
A6: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r / (abs a) by A1, A5, A3, XREAL_1:76;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
let n be Element of NAT ; :: thesis: ( k <= n implies ||.(((a * S) . n) - h).|| < r )
assume k <= n ; :: thesis: ||.(((a * S) . n) - h).|| < r
then A7: ||.((S . n) - g).|| < r / (abs a) by A6;
A8: 0 <> abs a by A4, COMPLEX1:133;
A9: (abs a) * (r / (abs a)) = (abs a) * (((abs a) " ) * r) by XCMPLX_0:def 9
.= ((abs a) * ((abs a) " )) * r
.= 1 * r by A8, XCMPLX_0:def 7
.= r ;
||.((a * (S . n)) - (a * g)).|| = ||.(a * ((S . n) - g)).|| by RLVECT_1:48
.= (abs a) * ||.((S . n) - g).|| by Def2 ;
then ||.((a * (S . n)) - h).|| < r by A5, A7, A9, XREAL_1:70;
hence ||.(((a * S) . n) - h).|| < r by Def8; :: thesis: verum

end;

now

assume A10: a = 0 ; :: thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
let r be Real; :: thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume 0 < r ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
then consider m1 being Element of NAT such that
A11: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
let n be Element of NAT ; :: thesis: ( k <= n implies ||.(((a * S) . n) - h).|| < r )
assume k <= n ; :: thesis: ||.(((a * S) . n) - h).|| < r
then A12: ||.((S . n) - g).|| < r by A11;
||.((a * (S . n)) - (a * g)).|| = ||.((0 * (S . n)) - H₁(RNS)).|| by A10, RLVECT_1:23
.= ||.(H₁(RNS) - H₁(RNS)).|| by RLVECT_1:23
.= ||.H₁(RNS).|| by RLVECT_1:26
.= 0 ;
then ||.((a * (S . n)) - h).|| < r by A12;
hence ||.(((a * S) . n) - h).|| < r by Def8; :: thesis: verum

end;

hence for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((a * S) . n) - h).|| < r by A2; :: thesis: verum