let S be RealNormSpace; :: thesis: for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent & seq is convergent holds
lim (rseq (#) seq) = (lim rseq) * (lim seq)
let rseq be Real_Sequence; :: thesis: for seq being sequence of S st rseq is convergent & seq is convergent holds
lim (rseq (#) seq) = (lim rseq) * (lim seq)
let seq be sequence of S; :: thesis: ( rseq is convergent & seq is convergent implies lim (rseq (#) seq) = (lim rseq) * (lim seq) )
assume that
A1: rseq is convergent and
A2: seq is convergent ; :: thesis: lim (rseq (#) seq) = (lim rseq) * (lim seq)
set g2 = lim seq;
reconsider g1 = lim rseq as Real ;
set g = g1 * (lim seq);
rseq is bounded by A1, SEQ_2:13;
then consider r being Real such that
A3: 0 < r and
A4: for n being Nat holds |.(rseq . n).| < r by SEQ_2:3;
reconsider r = r as Real ;
A5: 0 + 0 < ||.(lim seq).|| + r by A3, NORMSP_1:4, XREAL_1:8;
A6: 0 <= ||.(lim seq).|| by NORMSP_1:4;
A7: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
then A8: 0 < p / (||.(lim seq).|| + r) by A5, XREAL_1:139;
then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((rseq . m) - g1).| < p / (||.(lim seq).|| + r) by A1, SEQ_2:def 7;
consider n2 being Nat such that
A10: for m being Nat st n2 <= m holds
||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A2, A8, NORMSP_1:def 7;
take n = n1 + n2; :: thesis: for m being Nat st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
let m be Nat; :: thesis: ( n <= m implies ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p )
assume A11: n <= m ; :: thesis: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A12: |.((rseq . m) - g1).| <= p / (||.(lim seq).|| + r) by A9;
||.(((rseq . m) - g1) * (lim seq)).|| = ||.(lim seq).|| * |.((rseq . m) - g1).| by NORMSP_1:def 1;
then A13: ||.(((rseq . m) - g1) * (lim seq)).|| <= ||.(lim seq).|| * (p / (||.(lim seq).|| + r)) by A6, A12, XREAL_1:64;
A14: ( 0 <= |.(rseq . m).| & 0 <= ||.((seq . m) - (lim seq)).|| ) by COMPLEX1:46, NORMSP_1:4;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A15: ||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A10;
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| = ||.(((rseq . m) * (seq . m)) - (g1 * (lim seq))).|| by Def2
.= ||.((((rseq . m) * (seq . m)) - (0. S)) - (g1 * (lim seq))).|| by RLVECT_1:13
.= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * (lim seq)) - ((rseq . m) * (lim seq)))) - (g1 * (lim seq))).|| by RLVECT_1:15
.= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:29
.= ||.((((rseq . m) * ((seq . m) - (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:34
.= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) * (lim seq)) - (g1 * (lim seq)))).|| by RLVECT_1:def 3
.= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) - g1) * (lim seq))).|| by RLVECT_1:35 ;
then A16: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| <= ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| by NORMSP_1:def 1;
|.(rseq . m).| < r by A4;
then |.(rseq . m).| * ||.((seq . m) - (lim seq)).|| < r * (p / (||.(lim seq).|| + r)) by A14, A15, XREAL_1:96;
then A17: ||.((rseq . m) * ((seq . m) - (lim seq))).|| < r * (p / (||.(lim seq).|| + r)) by NORMSP_1:def 1;
(r * (p / (||.(lim seq).|| + r))) + (||.(lim seq).|| * (p / (||.(lim seq).|| + r))) = (p / (||.(lim seq).|| + r)) * (||.(lim seq).|| + r)
.= p by A5, XCMPLX_1:87 ;
then ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| < p by A17, A13, XREAL_1:8;
hence ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p by A16, XXREAL_0:2; :: thesis: verum

end;

rseq (#) seq is convergent by A1, A2, Th13;
hence lim (rseq (#) seq) = (lim rseq) * (lim seq) by A7, NORMSP_1:def 7; :: thesis: verum