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
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st Rseq is convergent & seq is convergent holds
Rseq * seq is convergent
let seq be sequence of X; :: thesis: ( Rseq is convergent & seq is convergent implies Rseq * seq is convergent )
assume that
A1: Rseq is convergent and
A2: seq is convergent ; :: thesis: Rseq * seq is convergent
consider p being real number such that
A3: for r being real number st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs ((Rseq . n) - p) < r by A1, SEQ_2:def 6;
reconsider p = p as Real by XREAL_0:def 1;
consider g being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r by A2, BHSP_2:9;

now

take h = p * g; :: thesis: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r
Rseq is bounded by A1, SEQ_2:27;
then consider b being real number such that
A5: b > 0 and
A6: for n being Element of NAT holds abs (Rseq . n) < b by SEQ_2:15;
reconsider b = b as Real by XREAL_0:def 1;
A7: ||.g.|| >= 0 by BHSP_1:34;
A8: b + ||.g.|| > 0 + 0 by A5, BHSP_1:34, XREAL_1:10;
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
||.(((Rseq * seq) . n) - h).|| < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r
then A9: r / (b + ||.g.||) > 0 by A8, XREAL_1:141;
then consider m1 being Element of NAT such that
A10: for n being Element of NAT st n >= m1 holds
abs ((Rseq . n) - p) < r / (b + ||.g.||) by A3;
consider m2 being Element of NAT such that
A11: for n being Element of NAT st n >= m2 holds
||.((seq . n) - g).|| < r / (b + ||.g.||) by A4, A9;
take m = m1 + m2; :: thesis: for n being Element of NAT st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r
let n be Element of NAT ; :: thesis: ( n >= m implies ||.(((Rseq * seq) . n) - h).|| < r )
assume A12: n >= m ; :: thesis: ||.(((Rseq * seq) . n) - h).|| < r
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A12, XXREAL_0:2;
then A13: abs ((Rseq . n) - p) <= r / (b + ||.g.||) by A10;
A14: abs (Rseq . n) < b by A6;
m >= m2 by NAT_1:12;
then n >= m2 by A12, XXREAL_0:2;
then A15: ||.((seq . n) - g).|| < r / (b + ||.g.||) by A11;
||.(((Rseq * seq) . n) - (p * g)).|| = ||.(((Rseq . n) * (seq . n)) - (p * g)).|| by Def9
.= ||.((((Rseq . n) * (seq . n)) - (p * g)) + H₁(X)).|| by RLVECT_1:10
.= ||.((((Rseq . n) * (seq . n)) - (p * g)) + (((Rseq . n) * g) - ((Rseq . n) * g))).|| by RLVECT_1:28
.= ||.(((Rseq . n) * (seq . n)) - ((p * g) - (((Rseq . n) * g) - ((Rseq . n) * g)))).|| by RLVECT_1:43
.= ||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * g) + ((p * g) - ((Rseq . n) * g)))).|| by RLVECT_1:43
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) - ((p * g) - ((Rseq . n) * g))).|| by RLVECT_1:41
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) + (((Rseq . n) * g) - (p * g))).|| by RLVECT_1:47 ;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * g)).|| + ||.(((Rseq . n) * g) - (p * g)).|| by BHSP_1:36;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) * g) - (p * g)).|| by RLVECT_1:48;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) - p) * g).|| by RLVECT_1:49;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= ((abs (Rseq . n)) * ||.((seq . n) - g).||) + ||.(((Rseq . n) - p) * g).|| by BHSP_1:33;
then A16: ||.(((Rseq * seq) . n) - (p * g)).|| <= ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) by BHSP_1:33;
A17: abs (Rseq . n) >= 0 by COMPLEX1:132;
||.((seq . n) - g).|| >= 0 by BHSP_1:34;
then A18: (abs (Rseq . n)) * ||.((seq . n) - g).|| < b * (r / (b + ||.g.||)) by A14, A15, A17, XREAL_1:98;
||.g.|| * (abs ((Rseq . n) - p)) <= ||.g.|| * (r / (b + ||.g.||)) by A7, A13, XREAL_1:66;
then ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < (b * (r / (b + ||.g.||))) + (||.g.|| * (r / (b + ||.g.||))) by A18, XREAL_1:10;
then ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b * r) / (b + ||.g.||)) + (||.g.|| * (r / (b + ||.g.||))) by XCMPLX_1:75;
then ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b * r) / (b + ||.g.||)) + ((||.g.|| * r) / (b + ||.g.||)) by XCMPLX_1:75;
then ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b * r) + (||.g.|| * r)) / (b + ||.g.||) by XCMPLX_1:63;
then ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < ((b + ||.g.||) * r) / (b + ||.g.||) ;
then ((abs (Rseq . n)) * ||.((seq . n) - g).||) + (||.g.|| * (abs ((Rseq . n) - p))) < r by A8, XCMPLX_1:90;
hence ||.(((Rseq * seq) . n) - h).|| < r by A16, XXREAL_0:2; :: thesis: verum

end;

hence Rseq * seq is convergent by BHSP_2:9; :: thesis: verum