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 number such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - g1) < p by A1, SEQ_2:def 6;
reconsider g1 = g1 as Real by XREAL_0:def 1;
consider g2 being Point of S such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - g2).|| < p by A2, NORMSP_1:def 9;
take g = g1 * g2; :: according to NORMSP_1:def 9 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= ||.(((rseq (#) seq) . b₃) - g).|| ) )
rseq is bounded by A1, SEQ_2:27;
then consider r being real number such that
A5: 0 < r and
A6: for n being Element of NAT holds abs (rseq . n) < r by SEQ_2:15;
reconsider r = r as Real by XREAL_0:def 1;
A7: 0 <= ||.g2.|| by NORMSP_1:8;
A8: 0 + 0 < ||.g2.|| + r by A5, NORMSP_1:8, XREAL_1:10;
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((rseq (#) seq) . b₂) - g).|| ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((rseq (#) seq) . b₂) - g).|| )
then A9: 0 < p / (||.g2.|| + r) by A8, XREAL_1:141;
then consider n1 being Element of NAT such that
A10: for m being Element of NAT st n1 <= m holds
abs ((rseq . m) - g1) < p / (||.g2.|| + r) by A3;
consider n2 being Element of NAT such that
A11: for m being Element of NAT st n2 <= m holds
||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A4, A9;
take n = n1 + n2; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= ||.(((rseq (#) seq) . b₁) - g).|| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= ||.(((rseq (#) seq) . m) - g).|| )
assume A12: n <= m ; :: thesis: not p <= ||.(((rseq (#) seq) . m) - g).||
A13: 0 <= abs (rseq . m) by COMPLEX1:132;
A14: 0 <= ||.((seq . m) - g2).|| by NORMSP_1:8;
n2 <= n by NAT_1:12;
then n2 <= m by A12, XXREAL_0:2;
then A15: ||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A11;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A12, XXREAL_0:2;
then A16: abs ((rseq . m) - g1) <= p / (||.g2.|| + r) by A10;
||.(((rseq (#) seq) . m) - g).|| = ||.(((rseq . m) * (seq . m)) - (g1 * g2)).|| by Def2
.= ||.((((rseq . m) * (seq . m)) - (0. S)) - (g1 * g2)).|| by RLVECT_1:26
.= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * g2) - ((rseq . m) * g2))) - (g1 * g2)).|| by RLVECT_1:28
.= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:43
.= ||.((((rseq . m) * ((seq . m) - g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:48
.= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) * g2) - (g1 * g2))).|| by RLVECT_1:def 6
.= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) - g1) * g2)).|| by RLVECT_1:49 ;
then A17: ||.(((rseq (#) seq) . m) - g).|| <= ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| by NORMSP_1:def 2;
abs (rseq . m) < r by A6;
then (abs (rseq . m)) * ||.((seq . m) - g2).|| < r * (p / (||.g2.|| + r)) by A13, A14, A15, XREAL_1:98;
then A18: ||.((rseq . m) * ((seq . m) - g2)).|| < r * (p / (||.g2.|| + r)) by NORMSP_1:def 2;
||.(((rseq . m) - g1) * g2).|| = ||.g2.|| * (abs ((rseq . m) - g1)) by NORMSP_1:def 2;
then A19: ||.(((rseq . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + r)) by A7, A16, XREAL_1:66;
(r * (p / (||.g2.|| + r))) + (||.g2.|| * (p / (||.g2.|| + r))) = (p / (||.g2.|| + r)) * (||.g2.|| + r)
.= p by A8, XCMPLX_1:88 ;
then ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| < p by A18, A19, XREAL_1:10;
hence not p <= ||.(((rseq (#) seq) . m) - g).|| by A17, XXREAL_0:2; :: thesis: verum