let X be ComplexUnitarySpace; :: thesis: for z being Complex
for seq being sequence of X st seq is convergent holds
lim (z * seq) = z * (lim seq)
let z be Complex; :: thesis: for seq being sequence of X st seq is convergent holds
lim (z * seq) = z * (lim seq)
let seq be sequence of X; :: thesis: ( seq is convergent implies lim (z * seq) = z * (lim seq) )
set g = lim seq;
set h = z * (lim seq);

A1: now :: thesis: ( z = 0 implies for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r )

set m1 = the Nat;
assume A2: z = 0 ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r )
assume A3: r > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
take k = the Nat; :: thesis: for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
let n be Nat; :: thesis: ( n >= k implies dist (((z * seq) . n),(z * (lim seq))) < r )
assume n >= k ; :: thesis: dist (((z * seq) . n),(z * (lim seq))) < r
dist ((z * (seq . n)),(z * (lim seq))) = dist ((0c * (seq . n)),H₁(X)) by A2, CLVECT_1:1
.= dist (H₁(X),H₁(X)) by CLVECT_1:1
.= 0 by CSSPACE:50 ;
hence dist (((z * seq) . n),(z * (lim seq))) < r by A3, CLVECT_1:def 14; :: thesis: verum

end;

assume A4: seq is convergent ; :: thesis: lim (z * seq) = z * (lim seq)

A5: now :: thesis: ( z <> 0 implies for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r )

A6: 0 / |.z.| = 0 ;
assume A7: z <> 0 ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
then A8: |.z.| > 0 by COMPLEX1:47;
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
then r / |.z.| > 0 by A8, A6, XREAL_1:74;
then consider m1 being Nat such that
A9: for n being Nat st n >= m1 holds
dist ((seq . n),(lim seq)) < r / |.z.| by A4, Def2;
take k = m1; :: thesis: for n being Nat st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
let n be Nat; :: thesis: ( n >= k implies dist (((z * seq) . n),(z * (lim seq))) < r )
assume n >= k ; :: thesis: dist (((z * seq) . n),(z * (lim seq))) < r
then A10: dist ((seq . n),(lim seq)) < r / |.z.| by A9;
A11: |.z.| <> 0 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 ;
dist ((z * (seq . n)),(z * (lim seq))) = ||.((z * (seq . n)) - (z * (lim seq))).|| by CSSPACE:def 16
.= ||.(z * ((seq . n) - (lim seq))).|| by CLVECT_1:9
.= |.z.| * ||.((seq . n) - (lim seq)).|| by CSSPACE:43
.= |.z.| * (dist ((seq . n),(lim seq))) by CSSPACE:def 16 ;
then dist ((z * (seq . n)),(z * (lim seq))) < r by A8, A10, A12, XREAL_1:68;
hence dist (((z * seq) . n),(z * (lim seq))) < r by CLVECT_1:def 14; :: thesis: verum

end;

z * seq is convergent by A4, Th5;
hence lim (z * seq) = z * (lim seq) by A1, A5, Def2; :: thesis: verum