let S be RealNormSpace; :: thesis: for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent & seq is convergent holds
rseq (#) seq is convergent
let rseq be Real_Sequence; :: thesis: for seq being sequence of S st rseq is convergent & seq is convergent holds
rseq (#) seq is convergent
let seq be sequence of S; :: 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 g1 being Real such that
A3: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((rseq . m) - g1).| < p by A1, SEQ_2:def 6;
consider g2 being Point of S such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - g2).|| < p by A2;
reconsider g1 = g1 as Real ;
take g = g1 * g2; :: according to NORMSP_1:def 6 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= ||.(((rseq (#) seq) . b₃) - g).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((rseq (#) seq) . b₂) - g).|| ) )
rseq is bounded by A1, SEQ_2:13;
then consider r being Real such that
A5: 0 < r and
A6: for n being Nat holds |.(rseq . n).| < r by SEQ_2:3;
reconsider r = r as Real ;
A7: 0 + 0 < ||.g2.|| + r by A5, NORMSP_1:4, XREAL_1:8;
assume A8: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((rseq (#) seq) . b₂) - g).|| )
then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((rseq . m) - g1).| < p / (||.g2.|| + r) by A3, A7, XREAL_1:139;
consider n2 being Nat such that
A10: for m being Nat st n2 <= m holds
||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A4, A7, A8, XREAL_1:139;
reconsider n = n1 + n2 as Nat ;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= ||.(((rseq (#) seq) . b₁) - g).|| )
let m be Nat; :: thesis: ( not n <= m or not p <= ||.(((rseq (#) seq) . m) - g).|| )
assume A11: n <= m ; :: thesis: not p <= ||.(((rseq (#) seq) . m) - g).||
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A12: |.((rseq . m) - g1).| <= p / (||.g2.|| + r) by A9;
( 0 <= ||.g2.|| & ||.(((rseq . m) - g1) * g2).|| = ||.g2.|| * |.((rseq . m) - g1).| ) by NORMSP_1:4, NORMSP_1:def 1;
then A13: ||.(((rseq . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + r)) by A12, XREAL_1:64;
||.(((rseq (#) seq) . m) - g).|| = ||.(((rseq . m) * (seq . m)) - (g1 * g2)).|| by Def2
.= ||.((((rseq . m) * (seq . m)) - (0. S)) - (g1 * g2)).|| by RLVECT_1:13
.= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * g2) - ((rseq . m) * g2))) - (g1 * g2)).|| by RLVECT_1:15
.= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:29
.= ||.((((rseq . m) * ((seq . m) - g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:34
.= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) * g2) - (g1 * g2))).|| by RLVECT_1:def 3
.= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) - g1) * g2)).|| by RLVECT_1:35 ;
then A14: ||.(((rseq (#) seq) . m) - g).|| <= ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| by NORMSP_1:def 1;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A15: ||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A10;
A16: ( 0 <= |.(rseq . m).| & 0 <= ||.((seq . m) - g2).|| ) by COMPLEX1:46, NORMSP_1:4;
|.(rseq . m).| < r by A6;
then |.(rseq . m).| * ||.((seq . m) - g2).|| < r * (p / (||.g2.|| + r)) by A16, A15, XREAL_1:96;
then A17: ||.((rseq . m) * ((seq . m) - g2)).|| < r * (p / (||.g2.|| + r)) by NORMSP_1:def 1;
(r * (p / (||.g2.|| + r))) + (||.g2.|| * (p / (||.g2.|| + r))) = (p / (||.g2.|| + r)) * (||.g2.|| + r)
.= p by A7, XCMPLX_1:87 ;
then ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| < p by A17, A13, XREAL_1:8;
hence not p <= ||.(((rseq (#) seq) . m) - g).|| by A14, XXREAL_0:2; :: thesis: verum