let a be Real; :: thesis: for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
lim (a * S) = a * (lim S)
let RNS be RealNormSpace; :: thesis: for S being sequence of RNS st S is convergent holds
lim (a * S) = a * (lim S)
let S be sequence of RNS; :: thesis: ( S is convergent implies lim (a * S) = a * (lim S) )
set g = lim S;
set h = a * (lim S);
assume A1: S is convergent ; :: thesis: lim (a * S) = a * (lim S)

A2: now

assume A3: 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) - (a * (lim S))).|| < 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) - (a * (lim S))).|| < 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) - (a * (lim S))).|| < r
then consider m1 being Element of NAT such that
A4: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r by A1, Def11;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
let n be Element of NAT ; :: thesis: ( k <= n implies ||.(((a * S) . n) - (a * (lim S))).|| < r )
assume k <= n ; :: thesis: ||.(((a * S) . n) - (a * (lim S))).|| < r
then A5: ||.((S . n) - (lim S)).|| < r by A4;
||.((a * (S . n)) - (a * (lim S))).|| = ||.((0 * (S . n)) - H₁(RNS)).|| by A3, RLVECT_1:10
.= ||.(H₁(RNS) - H₁(RNS)).|| by RLVECT_1:10
.= ||.H₁(RNS).|| by RLVECT_1:13
.= 0 ;
then ||.((a * (S . n)) - (a * (lim S))).|| < r by A5;
hence ||.(((a * S) . n) - (a * (lim S))).|| < r by Def8; :: thesis: verum

end;

A6: now

A7: 0 / (abs a) = 0 ;
assume A8: 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) - (a * (lim S))).|| < r
then A9: 0 < abs a by COMPLEX1:47;
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) - (a * (lim S))).|| < 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) - (a * (lim S))).|| < r
then 0 < r / (abs a) by A9, A7, XREAL_1:74;
then consider m1 being Element of NAT such that
A10: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r / (abs a) by A1, Def11;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
let n be Element of NAT ; :: thesis: ( k <= n implies ||.(((a * S) . n) - (a * (lim S))).|| < r )
assume k <= n ; :: thesis: ||.(((a * S) . n) - (a * (lim S))).|| < r
then A11: ||.((S . n) - (lim S)).|| < r / (abs a) by A10;
A12: 0 <> abs a by A8, COMPLEX1:47;
A13: (abs a) * (r / (abs a)) = (abs a) * (((abs a) ") * r) by XCMPLX_0:def 9
.= ((abs a) * ((abs a) ")) * r
.= 1 * r by A12, XCMPLX_0:def 7
.= r ;
||.((a * (S . n)) - (a * (lim S))).|| = ||.(a * ((S . n) - (lim S))).|| by RLVECT_1:34
.= (abs a) * ||.((S . n) - (lim S)).|| by Def2 ;
then ||.((a * (S . n)) - (a * (lim S))).|| < r by A9, A11, A13, XREAL_1:68;
hence ||.(((a * S) . n) - (a * (lim S))).|| < r by Def8; :: thesis: verum

end;

a * S is convergent by A1, Th37;
hence lim (a * S) = a * (lim S) by A2, A6, Def11; :: thesis: verum