let X be ComplexUnitarySpace; :: thesis: for z being Complex
for seq being sequence of X st seq is Cauchy holds
z * seq is Cauchy
let z be Complex; :: thesis: for seq being sequence of X st seq is Cauchy holds
z * seq is Cauchy
let seq be sequence of X; :: thesis: ( seq is Cauchy implies z * seq is Cauchy )
assume A1: seq is Cauchy ; :: thesis: z * seq is Cauchy

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

A3: 0 / |.z.| = 0 ;
assume A4: z <> 0 ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
then A5: |.z.| > 0 by COMPLEX1:47;
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
then r / |.z.| > 0 by A5, A3, XREAL_1:74;
then consider m1 being Nat such that
A6: for n, m being Nat st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r / |.z.| by A1;
take k = m1; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist (((z * seq) . n),((z * seq) . m)) < r )
assume ( n >= k & m >= k ) ; :: thesis: dist (((z * seq) . n),((z * seq) . m)) < r
then A7: dist ((seq . n),(seq . m)) < r / |.z.| by A6;
A8: |.z.| <> 0 by A4, COMPLEX1:47;
A9: |.z.| * (r / |.z.|) = |.z.| * ((|.z.| ") * r) by XCMPLX_0:def 9
.= (|.z.| * (|.z.| ")) * r
.= 1 * r by A8, XCMPLX_0:def 7
.= r ;
dist ((z * (seq . n)),(z * (seq . m))) = ||.((z * (seq . n)) - (z * (seq . m))).|| by CSSPACE:def 16
.= ||.(z * ((seq . n) - (seq . m))).|| by CLVECT_1:9
.= |.z.| * ||.((seq . n) - (seq . m)).|| by CSSPACE:43
.= |.z.| * (dist ((seq . n),(seq . m))) by CSSPACE:def 16 ;
then dist ((z * (seq . n)),(z * (seq . m))) < r by A5, A7, A9, XREAL_1:68;
then dist (((z * seq) . n),(z * (seq . m))) < r by CLVECT_1:def 14;
hence dist (((z * seq) . n),((z * seq) . m)) < r by CLVECT_1:def 14; :: thesis: verum

end;

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

assume A10: z = 0 ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
then consider m1 being Nat such that
A11: for n, m being Nat st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r by A1;
take k = m1; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist (((z * seq) . n),((z * seq) . m)) < r )
assume ( n >= k & m >= k ) ; :: thesis: dist (((z * seq) . n),((z * seq) . m)) < r
then A12: dist ((seq . n),(seq . m)) < r by A11;
dist ((z * (seq . n)),(z * (seq . m))) = dist (H₂(X),(0c * (seq . m))) by A10, CLVECT_1:1
.= dist (H₂(X),H₂(X)) by CLVECT_1:1
.= 0 by CSSPACE:50 ;
then dist ((z * (seq . n)),(z * (seq . m))) < r by A12, CSSPACE:53;
then dist (((z * seq) . n),(z * (seq . m))) < r by CLVECT_1:def 14;
hence dist (((z * seq) . n),((z * seq) . m)) < r by CLVECT_1:def 14; :: thesis: verum

end;

hence z * seq is Cauchy by A2; :: thesis: verum