let X be RealUnitarySpace; :: thesis: for a being Real
for seq being sequence of X st seq is convergent holds
a * seq is convergent
let a be Real; :: thesis: for seq being sequence of X st seq is convergent holds
a * seq is convergent
let seq be sequence of X; :: thesis: ( seq is convergent implies a * seq is convergent )
assume seq is convergent ; :: thesis: a * seq is convergent
then consider g being Point of X such that
A1: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),g) < r ;
take h = a * g; :: according to BHSP_2:def 1 :: thesis: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (((a * seq) . n),h) < r

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

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

assume A10: a = 0 ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
dist (((a * seq) . n),h) < r
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n being Nat st n >= k holds
dist (((a * seq) . n),h) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
dist (((a * seq) . n),h) < r
then consider m1 being Nat such that
A11: for n being Nat st n >= m1 holds
dist ((seq . n),g) < r by A1;
take k = m1; :: thesis: for n being Nat st n >= k holds
dist (((a * seq) . n),h) < r
let n be Nat; :: thesis: ( n >= k implies dist (((a * seq) . n),h) < r )
assume n >= k ; :: thesis: dist (((a * seq) . n),h) < r
then A12: dist ((seq . n),g) < r by A11;
dist ((a * (seq . n)),(a * g)) = dist ((0 * (seq . n)),H₁(X)) by A10, RLVECT_1:10
.= dist (H₁(X),H₁(X)) by RLVECT_1:10
.= 0 by BHSP_1:34 ;
then dist ((a * (seq . n)),h) < r by A12, BHSP_1:37;
hence dist (((a * seq) . n),h) < r by NORMSP_1:def 5; :: thesis: verum

end;

hence for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (((a * seq) . n),h) < r by A2; :: thesis: verum