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

A3: now

assume A4: a = 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 ((a * seq) . n),(a * (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 ((a * seq) . n),(a * (lim seq)) < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((a * seq) . n),(a * (lim seq)) < r
then consider m1 being Element of NAT such that
A5: for n being Element of NAT st n >= m1 holds
dist (seq . n),(lim seq) < r by A1, Def2;
take k = m1; :: thesis: for n being Element of NAT st n >= k holds
dist ((a * seq) . n),(a * (lim seq)) < r
let n be Element of 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 A6: dist (seq . n),(lim seq) < r by A5;
dist (a * (seq . n)),(a * (lim seq)) = dist (0 * (seq . n)),H₁(X) by A4, RLVECT_1:23
.= dist H₁(X),H₁(X) by RLVECT_1:23
.= 0 by BHSP_1:41 ;
then dist (a * (seq . n)),(a * (lim seq)) < r by A6, BHSP_1:44;
hence dist ((a * seq) . n),(a * (lim seq)) < r by NORMSP_1:def 8; :: thesis: verum

end;

now

assume A7: a <> 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 ((a * seq) . n),(a * (lim seq)) < r
then A8: abs a > 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 ((a * seq) . n),(a * (lim seq)) < r )
assume A9: r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((a * seq) . n),(a * (lim seq)) < r
A10: abs a <> 0 by A7, COMPLEX1:133;
0 / (abs a) = 0 ;
then r / (abs a) > 0 by A8, A9, XREAL_1:76;
then consider m1 being Element of NAT such that
A11: for n being Element of NAT st n >= m1 holds
dist (seq . n),(lim seq) < r / (abs a) by A1, Def2;
take k = m1; :: thesis: for n being Element of NAT st n >= k holds
dist ((a * seq) . n),(a * (lim seq)) < r
let n be Element of 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 A12: dist (seq . n),(lim seq) < r / (abs a) by A11;
A13: 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:48
.= (abs a) * ||.((seq . n) - (lim seq)).|| by BHSP_1:33
.= (abs a) * (dist (seq . n),(lim seq)) by BHSP_1:def 5 ;
(abs a) * (r / (abs a)) = (abs a) * (((abs a) " ) * r) by XCMPLX_0:def 9
.= ((abs a) * ((abs a) " )) * r
.= 1 * r by A10, XCMPLX_0:def 7
.= r ;
then dist (a * (seq . n)),(a * (lim seq)) < r by A8, A12, A13, XREAL_1:70;
hence dist ((a * seq) . n),(a * (lim seq)) < r by NORMSP_1:def 8; :: thesis: verum

end;

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