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) )
assume A1: seq is convergent ; :: thesis: lim (z * seq) = z * (lim seq)
then A2: z * seq is convergent by Th5;
set g = lim seq;
set h = z * (lim seq);

A3: now

assume A4: z = 0 ; :: thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r
let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r )
assume A5: r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r
consider m1 being Element of NAT ;
take k = m1; :: thesis: for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r
let n be Element of 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 A4, CLVECT_1:2
.= dist H₁(X),H₁(X) by CLVECT_1:2
.= 0 by CSSPACE:53 ;
hence dist ((z * seq) . n),(z * (lim seq)) < r by A5, CLVECT_1:def 15; :: thesis: verum

end;

now

assume A6: z <> 0 ; :: thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r
then A7: |.z.| > 0 by COMPLEX1:133;
let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r )
assume A8: r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r
A9: |.z.| <> 0 by A6, COMPLEX1:133;
0 / |.z.| = 0 ;
then r / |.z.| > 0 by A7, A8, XREAL_1:76;
then consider m1 being Element of NAT such that
A10: for n being Element of NAT st n >= m1 holds
dist (seq . n),(lim seq) < r / |.z.| by A1, Def2;
take k = m1; :: thesis: for n being Element of NAT st n >= k holds
dist ((z * seq) . n),(z * (lim seq)) < r
let n be Element of 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 A11: dist (seq . n),(lim seq) < r / |.z.| by A10;
A12: 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:10
.= |.z.| * ||.((seq . n) - (lim seq)).|| by CSSPACE:45
.= |.z.| * (dist (seq . n),(lim seq)) by CSSPACE:def 16 ;
|.z.| * (r / |.z.|) = |.z.| * ((|.z.| " ) * r) by XCMPLX_0:def 9
.= (|.z.| * (|.z.| " )) * r
.= 1 * r by A9, XCMPLX_0:def 7
.= r ;
then dist (z * (seq . n)),(z * (lim seq)) < r by A7, A11, A12, XREAL_1:70;
hence dist ((z * seq) . n),(z * (lim seq)) < r by CLVECT_1:def 15; :: thesis: verum

end;

hence lim (z * seq) = z * (lim seq) by A2, A3, Def2; :: thesis: verum