let X be RealUnitarySpace; :: thesis: for a being Real

for seq being sequence of X st seq is convergent holds

lim (a * seq) = a * (lim seq)

let a be Real; :: thesis: for seq being sequence of X st seq is convergent holds

lim (a * seq) = a * (lim seq)

let seq be sequence of X; :: thesis: ( seq is convergent implies lim (a * seq) = a * (lim seq) )

set g = lim seq;

set h = a * (lim seq);

assume A1: seq is convergent ; :: thesis: lim (a * seq) = a * (lim seq)

hence lim (a * seq) = a * (lim seq) by A2, A6, Def2; :: thesis: verum

for seq being sequence of X st seq is convergent holds

lim (a * seq) = a * (lim seq)

let a be Real; :: thesis: for seq being sequence of X st seq is convergent holds

lim (a * seq) = a * (lim seq)

let seq be sequence of X; :: thesis: ( seq is convergent implies lim (a * seq) = a * (lim seq) )

set g = lim seq;

set h = a * (lim seq);

assume A1: seq is convergent ; :: thesis: lim (a * seq) = a * (lim seq)

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),(a * (lim seq))) < r )

ex k being Nat st

for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r )

assume A3:
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),(a * (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 (((a * seq) . n),(a * (lim seq))) < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

then consider m1 being Nat such that

A4: for n being Nat st n >= m1 holds

dist ((seq . n),(lim seq)) < r by A1, Def2;

take k = m1; :: thesis: for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

let n be Nat; :: thesis: ( n >= k implies dist (((a * seq) . n),(a * (lim seq))) < r )

assume n >= k ; :: thesis: dist (((a * seq) . n),(a * (lim seq))) < r

then A5: dist ((seq . n),(lim seq)) < r by A4;

dist ((a * (seq . n)),(a * (lim seq))) = dist ((0 * (seq . n)),H_{1}(X))
by A3, RLVECT_1:10

.= dist (H_{1}(X),H_{1}(X))
by RLVECT_1:10

.= 0 by BHSP_1:34 ;

then dist ((a * (seq . n)),(a * (lim seq))) < r by A5, BHSP_1:37;

hence dist (((a * seq) . n),(a * (lim seq))) < r by NORMSP_1:def 5; :: thesis: verum

end;ex k being Nat st

for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (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 (((a * seq) . n),(a * (lim seq))) < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

then consider m1 being Nat such that

A4: for n being Nat st n >= m1 holds

dist ((seq . n),(lim seq)) < r by A1, Def2;

take k = m1; :: thesis: for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

let n be Nat; :: thesis: ( n >= k implies dist (((a * seq) . n),(a * (lim seq))) < r )

assume n >= k ; :: thesis: dist (((a * seq) . n),(a * (lim seq))) < r

then A5: dist ((seq . n),(lim seq)) < r by A4;

dist ((a * (seq . n)),(a * (lim seq))) = dist ((0 * (seq . n)),H

.= dist (H

.= 0 by BHSP_1:34 ;

then dist ((a * (seq . n)),(a * (lim seq))) < r by A5, BHSP_1:37;

hence dist (((a * seq) . n),(a * (lim seq))) < r by NORMSP_1:def 5; :: thesis: verum

A6: 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),(a * (lim seq))) < r )

a * seq is convergent
by A1, Th5;ex k being Nat st

for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r )

A7:
0 / |.a.| = 0
;

assume A8: 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),(a * (lim seq))) < r

then A9: |.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),(a * (lim seq))) < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

then r / |.a.| > 0 by A9, A7, XREAL_1:74;

then consider m1 being Nat such that

A10: for n being Nat st n >= m1 holds

dist ((seq . n),(lim seq)) < r / |.a.| by A1, Def2;

take k = m1; :: thesis: for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

let n be Nat; :: thesis: ( n >= k implies dist (((a * seq) . n),(a * (lim seq))) < r )

assume n >= k ; :: thesis: dist (((a * seq) . n),(a * (lim seq))) < r

then A11: dist ((seq . n),(lim seq)) < r / |.a.| by A10;

A12: |.a.| <> 0 by A8, COMPLEX1:47;

A13: |.a.| * (r / |.a.|) = |.a.| * ((|.a.| ") * r) by XCMPLX_0:def 9

.= (|.a.| * (|.a.| ")) * r

.= 1 * r by A12, XCMPLX_0:def 7

.= r ;

dist ((a * (seq . n)),(a * (lim seq))) = ||.((a * (seq . n)) - (a * (lim seq))).|| by BHSP_1:def 5

.= ||.(a * ((seq . n) - (lim seq))).|| by RLVECT_1:34

.= |.a.| * ||.((seq . n) - (lim seq)).|| by BHSP_1:27

.= |.a.| * (dist ((seq . n),(lim seq))) by BHSP_1:def 5 ;

then dist ((a * (seq . n)),(a * (lim seq))) < r by A9, A11, A13, XREAL_1:68;

hence dist (((a * seq) . n),(a * (lim seq))) < r by NORMSP_1:def 5; :: thesis: verum

end;assume A8: 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),(a * (lim seq))) < r

then A9: |.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),(a * (lim seq))) < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

then r / |.a.| > 0 by A9, A7, XREAL_1:74;

then consider m1 being Nat such that

A10: for n being Nat st n >= m1 holds

dist ((seq . n),(lim seq)) < r / |.a.| by A1, Def2;

take k = m1; :: thesis: for n being Nat st n >= k holds

dist (((a * seq) . n),(a * (lim seq))) < r

let n be Nat; :: thesis: ( n >= k implies dist (((a * seq) . n),(a * (lim seq))) < r )

assume n >= k ; :: thesis: dist (((a * seq) . n),(a * (lim seq))) < r

then A11: dist ((seq . n),(lim seq)) < r / |.a.| by A10;

A12: |.a.| <> 0 by A8, COMPLEX1:47;

A13: |.a.| * (r / |.a.|) = |.a.| * ((|.a.| ") * r) by XCMPLX_0:def 9

.= (|.a.| * (|.a.| ")) * r

.= 1 * r by A12, XCMPLX_0:def 7

.= r ;

dist ((a * (seq . n)),(a * (lim seq))) = ||.((a * (seq . n)) - (a * (lim seq))).|| by BHSP_1:def 5

.= ||.(a * ((seq . n) - (lim seq))).|| by RLVECT_1:34

.= |.a.| * ||.((seq . n) - (lim seq)).|| by BHSP_1:27

.= |.a.| * (dist ((seq . n),(lim seq))) by BHSP_1:def 5 ;

then dist ((a * (seq . n)),(a * (lim seq))) < r by A9, A11, A13, XREAL_1:68;

hence dist (((a * seq) . n),(a * (lim seq))) < r by NORMSP_1:def 5; :: thesis: verum

hence lim (a * seq) = a * (lim seq) by A2, A6, Def2; :: thesis: verum