let z be Complex; :: thesis: for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
lim (z * S) = z * (lim S)
let CNS be ComplexNormSpace; :: thesis: for S being sequence of CNS st S is convergent holds
lim (z * S) = z * (lim S)
let S be sequence of CNS; :: thesis: ( S is convergent implies lim (z * S) = z * (lim S) )
set g = lim S;
set h = z * (lim S);
assume A1: S is convergent ; :: thesis: lim (z * S) = z * (lim S)

A2: now :: thesis: ( z = 0 implies for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r )

assume A3: z = 0 ; :: thesis: for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r )
assume 0 < r ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
then consider m1 being Nat such that
A4: for n being Nat st m1 <= n holds
||.((S . n) - (lim S)).|| < r by A1, Def16;
take k = m1; :: thesis: for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
let n be Nat; :: thesis: ( k <= n implies ||.(((z * S) . n) - (z * (lim S))).|| < r )
assume k <= n ; :: thesis: ||.(((z * S) . n) - (z * (lim S))).|| < r
then A5: ||.((S . n) - (lim S)).|| < r by A4;
||.((z * (S . n)) - (z * (lim S))).|| = ||.((0c * (S . n)) - H₁(CNS)).|| by A3, Th1
.= ||.(H₁(CNS) - H₁(CNS)).|| by Th1
.= ||.H₁(CNS).|| by RLVECT_1:13
.= 0 ;
then ||.((z * (S . n)) - (z * (lim S))).|| < r by A5, Th105;
hence ||.(((z * S) . n) - (z * (lim S))).|| < r by Def14; :: thesis: verum

end;

A6: now :: thesis: ( z <> 0c implies for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r )

assume A7: z <> 0c ; :: thesis: for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
then A8: 0 < |.z.| by COMPLEX1:47;
let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r )
assume 0 < r ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
then consider m1 being Nat such that
A9: for n being Nat st m1 <= n holds
||.((S . n) - (lim S)).|| < r / |.z.| by A1, A8, Def16;
take k = m1; :: thesis: for n being Nat st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
let n be Nat; :: thesis: ( k <= n implies ||.(((z * S) . n) - (z * (lim S))).|| < r )
assume k <= n ; :: thesis: ||.(((z * S) . n) - (z * (lim S))).|| < r
then A10: ||.((S . n) - (lim S)).|| < r / |.z.| by A9;
A11: 0 <> |.z.| by A7, COMPLEX1:47;
A12: |.z.| * (r / |.z.|) = |.z.| * ((|.z.| ") * r) by XCMPLX_0:def 9
.= (|.z.| * (|.z.| ")) * r
.= 1 * r by A11, XCMPLX_0:def 7
.= r ;
||.((z * (S . n)) - (z * (lim S))).|| = ||.(z * ((S . n) - (lim S))).|| by Th9
.= |.z.| * ||.((S . n) - (lim S)).|| by Def13 ;
then ||.((z * (S . n)) - (z * (lim S))).|| < r by A8, A10, A12, XREAL_1:68;
hence ||.(((z * S) . n) - (z * (lim S))).|| < r by Def14; :: thesis: verum

end;

z * S is convergent by A1, Th116;
hence lim (z * S) = z * (lim S) by A2, A6, Def16; :: thesis: verum