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 such that
A3: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
|.((Rseq . n) - p).| < r by A1, SEQ_2:def 6;
consider g being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g).|| < r by A2, BHSP_2:9;
reconsider p = p as Real ;

now :: thesis: ex h being Element of the carrier of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r

take h = p * g; :: thesis: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r
let r be Real; :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r )
consider b being Real such that
A5: b > 0 and
A6: for n being Nat holds |.(Rseq . n).| < b by A1, SEQ_2:3, SEQ_2:13;
reconsider b = b as Real ;
A7: b + ||.g.|| > 0 + 0 by A5, BHSP_1:28, XREAL_1:8;
assume A8: r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r
then consider m1 being Nat such that
A9: for n being Nat st n >= m1 holds
|.((Rseq . n) - p).| < r / (b + ||.g.||) by A3, A7, XREAL_1:139;
consider m2 being Nat such that
A10: for n being Nat st n >= m2 holds
||.((seq . n) - g).|| < r / (b + ||.g.||) by A4, A7, A8, XREAL_1:139;
reconsider m = m1 + m2 as Nat ;
take m = m; :: thesis: for n being Nat st n >= m holds
||.(((Rseq * seq) . n) - h).|| < r
let n be Nat; :: thesis: ( n >= m implies ||.(((Rseq * seq) . n) - h).|| < r )
assume A11: n >= m ; :: thesis: ||.(((Rseq * seq) . n) - h).|| < r
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A11, XXREAL_0:2;
then ( ||.g.|| >= 0 & |.((Rseq . n) - p).| <= r / (b + ||.g.||) ) by A9, BHSP_1:28;
then A12: ||.g.|| * |.((Rseq . n) - p).| <= ||.g.|| * (r / (b + ||.g.||)) by XREAL_1:64;
A13: ( |.(Rseq . n).| >= 0 & ||.((seq . n) - g).|| >= 0 ) by BHSP_1:28, COMPLEX1:46;
m >= m2 by NAT_1:12;
then n >= m2 by A11, XXREAL_0:2;
then A14: ||.((seq . n) - g).|| < r / (b + ||.g.||) by A10;
|.(Rseq . n).| < b by A6;
then |.(Rseq . n).| * ||.((seq . n) - g).|| < b * (r / (b + ||.g.||)) by A14, A13, XREAL_1:96;
then (|.(Rseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Rseq . n) - p).|) < (b * (r / (b + ||.g.||))) + (||.g.|| * (r / (b + ||.g.||))) by A12, XREAL_1:8;
then (|.(Rseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Rseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + (||.g.|| * (r / (b + ||.g.||))) by XCMPLX_1:74;
then (|.(Rseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Rseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + ((||.g.|| * r) / (b + ||.g.||)) by XCMPLX_1:74;
then (|.(Rseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Rseq . n) - p).|) < ((b * r) + (||.g.|| * r)) / (b + ||.g.||) by XCMPLX_1:62;
then (|.(Rseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Rseq . n) - p).|) < ((b + ||.g.||) * r) / (b + ||.g.||) ;
then A15: (|.(Rseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Rseq . n) - p).|) < r by A7, XCMPLX_1:89;
||.(((Rseq * seq) . n) - (p * g)).|| = ||.(((Rseq . n) * (seq . n)) - (p * g)).|| by Def7
.= ||.((((Rseq . n) * (seq . n)) - (p * g)) + H₁(X)).||
.= ||.((((Rseq . n) * (seq . n)) - (p * g)) + (((Rseq . n) * g) - ((Rseq . n) * g))).|| by RLVECT_1:15
.= ||.(((Rseq . n) * (seq . n)) - ((p * g) - (((Rseq . n) * g) - ((Rseq . n) * g)))).|| by RLVECT_1:29
.= ||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * g) + ((p * g) - ((Rseq . n) * g)))).|| by RLVECT_1:29
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) - ((p * g) - ((Rseq . n) * g))).|| by RLVECT_1:27
.= ||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * g)) + (((Rseq . n) * g) - (p * g))).|| by RLVECT_1:33 ;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * g)).|| + ||.(((Rseq . n) * g) - (p * g)).|| by BHSP_1:30;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) * g) - (p * g)).|| by RLVECT_1:34;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= ||.((Rseq . n) * ((seq . n) - g)).|| + ||.(((Rseq . n) - p) * g).|| by RLVECT_1:35;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= (|.(Rseq . n).| * ||.((seq . n) - g).||) + ||.(((Rseq . n) - p) * g).|| by BHSP_1:27;
then ||.(((Rseq * seq) . n) - (p * g)).|| <= (|.(Rseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Rseq . n) - p).|) by BHSP_1:27;
hence ||.(((Rseq * seq) . n) - h).|| < r by A15, XXREAL_0:2; :: thesis: verum

end;

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