A1: now :: thesis: ( a <> 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 (((a * seq) . n),((a * seq) . m)) < r )

A2: 0 / |.a.| = 0 ;
assume A3: a <> 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 (((a * seq) . n),((a * seq) . m)) < r
then A4: |.a.| > 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 (((a * seq) . n),((a * seq) . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((a * seq) . n),((a * seq) . m)) < r
then r / |.a.| > 0 by A4, A2, XREAL_1:74;
then consider m1 being Nat such that
A5: for n, m being Nat st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r / |.a.| by Def1;
take k = m1; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist (((a * seq) . n),((a * seq) . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist (((a * seq) . n),((a * seq) . m)) < r )
assume ( n >= k & m >= k ) ; :: thesis: dist (((a * seq) . n),((a * seq) . m)) < r
then A6: dist ((seq . n),(seq . m)) < r / |.a.| by A5;
A7: |.a.| <> 0 by A3, COMPLEX1:47;
A8: |.a.| * (r / |.a.|) = |.a.| * ((|.a.| ") * r) by XCMPLX_0:def 9
.= (|.a.| * (|.a.| ")) * r
.= 1 * r by A7, XCMPLX_0:def 7
.= r ;
dist ((a * (seq . n)),(a * (seq . m))) = ||.((a * (seq . n)) - (a * (seq . m))).|| by BHSP_1:def 5
.= ||.(a * ((seq . n) - (seq . m))).|| by RLVECT_1:34
.= |.a.| * ||.((seq . n) - (seq . m)).|| by BHSP_1:27
.= |.a.| * (dist ((seq . n),(seq . m))) by BHSP_1:def 5 ;
then dist ((a * (seq . n)),(a * (seq . m))) < r by A4, A6, A8, XREAL_1:68;
then dist (((a * seq) . n),(a * (seq . m))) < r by NORMSP_1:def 5;
hence dist (((a * seq) . n),((a * seq) . m)) < r by NORMSP_1:def 5; :: thesis: verum

end;

now :: thesis: ( a = 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 (((a * seq) . n),((a * seq) . m)) < r )

assume A9: a = 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 (((a * seq) . n),((a * 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 (((a * seq) . n),((a * seq) . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((a * seq) . n),((a * seq) . m)) < r
then consider m1 being Nat such that
A10: for n, m being Nat st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r by Def1;
take k = m1; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist (((a * seq) . n),((a * seq) . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist (((a * seq) . n),((a * seq) . m)) < r )
assume ( n >= k & m >= k ) ; :: thesis: dist (((a * seq) . n),((a * seq) . m)) < r
then A11: dist ((seq . n),(seq . m)) < r by A10;
dist ((a * (seq . n)),(a * (seq . m))) = dist (H₁(X),(0 * (seq . m))) by A9, RLVECT_1:10
.= dist (H₁(X),H₁(X)) by RLVECT_1:10
.= 0 by BHSP_1:34 ;
then dist ((a * (seq . n)),(a * (seq . m))) < r by A11, BHSP_1:37;
then dist (((a * seq) . n),(a * (seq . m))) < r by NORMSP_1:def 5;
hence dist (((a * seq) . n),((a * seq) . m)) < r by NORMSP_1:def 5; :: thesis: verum

end;

hence a * seq is Cauchy by A1; :: thesis: verum