let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
let seq be sequence of X; :: thesis: ( Rseq is convergent & seq is convergent implies ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) ) )
assume that
A1: Rseq is convergent and
A2: seq is convergent ; :: thesis: ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
Rseq is bounded by A1, SEQ_2:13;
then consider b being real number such that
A3: b > 0 and
A4: for n being Element of NAT holds abs (Rseq . n) < b by SEQ_2:3;
reconsider b = b as Real by XREAL_0:def 1;
A5: b + ||.(lim seq).|| > 0 + 0 by A3, BHSP_1:28, XREAL_1:8;
A6: ||.(lim seq).|| >= 0 by BHSP_1:28;

A7: now

let r be Real; :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r
then A8: r / (b + ||.(lim seq).||) > 0 by A5, XREAL_1:139;
then consider m1 being Element of NAT such that
A9: for n being Element of NAT st n >= m1 holds
abs ((Rseq . n) - (lim Rseq)) < r / (b + ||.(lim seq).||) by A1, SEQ_2:def 7;
consider m2 being Element of NAT such that
A10: for n being Element of NAT st n >= m2 holds
dist ((seq . n),(lim seq)) < r / (b + ||.(lim seq).||) by A2, A8, BHSP_2:def 2;
take m = m1 + m2; :: thesis: for n being Element of NAT st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r
let n be Element of NAT ; :: thesis: ( n >= m implies dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r )
assume A11: n >= m ; :: thesis: dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A11, XXREAL_0:2;
then abs ((Rseq . n) - (lim Rseq)) <= r / (b + ||.(lim seq).||) by A9;
then A12: ||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq))) <= ||.(lim seq).|| * (r / (b + ||.(lim seq).||)) by A6, XREAL_1:64;
A13: ||.((seq . n) - (lim seq)).|| >= 0 by BHSP_1:28;
m >= m2 by NAT_1:12;
then n >= m2 by A11, XXREAL_0:2;
then dist ((seq . n),(lim seq)) < r / (b + ||.(lim seq).||) by A10;
then A14: ||.((seq . n) - (lim seq)).|| < r / (b + ||.(lim seq).||) by BHSP_1:def 5;
( abs (Rseq . n) < b & abs (Rseq . n) >= 0 ) by A4, COMPLEX1:46;
then (abs (Rseq . n)) * ||.((seq . n) - (lim seq)).|| < b * (r / (b + ||.(lim seq).||)) by A14, A13, XREAL_1:96;
then ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < (b * (r / (b + ||.(lim seq).||))) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by A12, XREAL_1:8;
then ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b * r) / (b + ||.(lim seq).||)) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||))) by XCMPLX_1:74;
then ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b * r) / (b + ||.(lim seq).||)) + ((||.(lim seq).|| * r) / (b + ||.(lim seq).||)) by XCMPLX_1:74;
then ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b * r) + (||.(lim seq).|| * r)) / (b + ||.(lim seq).||) by XCMPLX_1:62;
then ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < ((b + ||.(lim seq).||) * r) / (b + ||.(lim seq).||) ;
then A15: ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) < r by A5, XCMPLX_1:89;
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| = ||.(((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))).|| by Def9
.= ||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + H₁(X)).|| by RLVECT_1:4
.= ||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)))).|| by RLVECT_1:15
.= ||.(((Rseq . n) * (seq . n)) - (((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))))).|| by RLVECT_1:29
.= ||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))))).|| by RLVECT_1:29
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) - (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)))).|| by RLVECT_1:27
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq)))).|| by RLVECT_1:33 ;
then ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).|| by BHSP_1:30;
then ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).|| by RLVECT_1:34;
then ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).|| by RLVECT_1:35;
then ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).|| by BHSP_1:27;
then ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ((abs (Rseq . n)) * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * (abs ((Rseq . n) - (lim Rseq)))) by BHSP_1:27;
then ||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| < r by A15, XXREAL_0:2;
hence dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r by BHSP_1:def 5; :: thesis: verum

end;

Rseq * seq is convergent by A1, A2, Th50;
hence ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) ) by A7, BHSP_2:def 2; :: thesis: verum