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 ;
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 b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= ||.(((rseq (#) seq) . b3) - g).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.(((rseq (#) seq) . b2) - g).|| ) )

rseq is bounded by ;
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 ;
assume A8: 0 < p ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.(((rseq (#) seq) . b2) - g).|| )

then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((rseq . m) - g1).| < p / (||.g2.|| + r) by ;
consider n2 being Nat such that
A10: for m being Nat st n2 <= m holds
||.((seq . m) - g2).|| < p / (||.g2.|| + r) by ;
reconsider n = n1 + n2 as Nat ;
take n ; :: thesis: for b1 being set holds
( not n <= b1 or not p <= ||.(((rseq (#) seq) . b1) - 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 ;
then A12: |.((rseq . m) - g1).| <= p / (||.g2.|| + r) by A9;
( 0 <= ||.g2.|| & ||.(((rseq . m) - g1) * g2).|| = ||.g2.|| * |.((rseq . m) - g1).| ) by ;
then A13: ||.(((rseq . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + r)) by ;
||.(((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 ;
then A15: ||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A10;
A16: ( 0 <= |.(rseq . m).| & 0 <= ||.((seq . m) - g2).|| ) by ;
|.(rseq . m).| < r by A6;
then |.(rseq . m).| * ||.((seq . m) - g2).|| < r * (p / (||.g2.|| + r)) by ;
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 ;
then ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| < p by ;
hence not p <= ||.(((rseq (#) seq) . m) - g).|| by ; :: thesis: verum