let z be Complex; :: thesis: for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
z * S is convergent
let CNS be ComplexNormSpace; :: thesis: for S being sequence of CNS st S is convergent holds
z * S is convergent
let S be sequence of CNS; :: thesis: ( S is convergent implies z * S is convergent )
assume S is convergent ; :: thesis: z * S is convergent
then consider g being Point of CNS 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 Def16;
take h = z * g; :: according to CLVECT_1:def 16 :: 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
||.(((z * S) . n) - h).|| < r

A2: now

assume A3: z = 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
||.(((z * 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
||.(((z * 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
||.(((z * S) . n) - h).|| < r
then consider m1 being Element of NAT such that
A4: 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
||.(((z * S) . n) - h).|| < r
let n be Element of NAT ; :: thesis: ( k <= n implies ||.(((z * S) . n) - h).|| < r )
assume k <= n ; :: thesis: ||.(((z * S) . n) - h).|| < r
then A5: ||.((S . n) - g).|| < r by A4;
||.((z * (S . n)) - (z * g)).|| = ||.((0c * (S . n)) - H₁(CNS)).|| by A3, Th2
.= ||.(H₁(CNS) - H₁(CNS)).|| by Th2
.= ||.H₁(CNS).|| by RLVECT_1:26
.= 0 by Def11 ;
then ||.((z * (S . n)) - h).|| < r by A5, Th106;
hence ||.(((z * S) . n) - h).|| < r by Def15; :: thesis: verum

end;

now

assume A6: z <> 0c ; :: 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
||.(((z * S) . n) - h).|| < r
then A7: 0 < |.z.| 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
||.(((z * S) . n) - h).|| < r )
assume A8: 0 < r ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
A9: 0 <> |.z.| by A6, COMPLEX1:133;
0 < r / |.z.| by A7, A8;
then consider m1 being Element of NAT such that
A10: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r / |.z.| by A1;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
let n be Element of NAT ; :: thesis: ( k <= n implies ||.(((z * S) . n) - h).|| < r )
assume k <= n ; :: thesis: ||.(((z * S) . n) - h).|| < r
then A11: ||.((S . n) - g).|| < r / |.z.| by A10;
A12: ||.((z * (S . n)) - (z * g)).|| = ||.(z * ((S . n) - g)).|| by Th10
.= |.z.| * ||.((S . n) - g).|| by Def11 ;
|.z.| * (r / |.z.|) = |.z.| * ((|.z.| " ) * r) by XCMPLX_0:def 9
.= (|.z.| * (|.z.| " )) * r
.= 1 * r by A9, XCMPLX_0:def 7
.= r ;
then ||.((z * (S . n)) - h).|| < r by A7, A11, A12, XREAL_1:70;
hence ||.(((z * S) . n) - h).|| < r by Def15; :: 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
||.(((z * S) . n) - h).|| < r by A2; :: thesis: verum