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_{1} being object holds

( b_{1} <= 0 or ex b_{2} being set st

for b_{3} being set holds

( not b_{2} <= b_{3} or not b_{1} <= ||.(((rseq (#) seq) . b_{3}) - g).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.(((rseq (#) seq) . b_{2}) - 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_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.(((rseq (#) seq) . b_{2}) - 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_{1} being set holds

( not n <= b_{1} or not p <= ||.(((rseq (#) seq) . b_{1}) - 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

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

( b

for b

( not b

let p be Real; :: thesis: ( p <= 0 or ex b

for b

( not b

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

for b

( not b

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

( not n <= b

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