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)
reconsider g1 = lim rseq as Real ;
set g2 = lim seq;
set g = g1 * (lim seq);
rseq is bounded by A1, SEQ_2:27;
then consider r being real number such that
A3: 0 < r and
A4: 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;
A5: 0 <= ||.(lim seq).|| by NORMSP_1:8;
A6: 0 + 0 < ||.(lim seq).|| + r by A3, NORMSP_1:8, XREAL_1:10;
A7: rseq (#) seq is convergent by A1, A2, Th13;
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
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
then A8: 0 < p / (||.(lim seq).|| + r) by A6, XREAL_1:141;
then consider n1 being Element of NAT such that
A9: for m being Element of NAT st n1 <= m holds
abs ((rseq . m) - g1) < p / (||.(lim seq).|| + r) by A1, SEQ_2:def 7;
consider n2 being Element of NAT such that
A10: for m being Element of NAT st n2 <= m holds
||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A2, A8, NORMSP_1:def 11;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p )
assume A11: n <= m ; :: thesis: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
A12: 0 <= abs (rseq . m) by COMPLEX1:132;
A13: 0 <= ||.((seq . m) - (lim seq)).|| by NORMSP_1:8;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A14: ||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A10;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A15: abs ((rseq . m) - g1) <= p / (||.(lim seq).|| + r) by A9;
||.(((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:26
.= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * (lim seq)) - ((rseq . m) * (lim seq)))) - (g1 * (lim seq))).|| by RLVECT_1:28
.= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:43
.= ||.((((rseq . m) * ((seq . m) - (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:48
.= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) * (lim seq)) - (g1 * (lim seq)))).|| by RLVECT_1:def 6
.= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) - g1) * (lim seq))).|| by RLVECT_1:49 ;
then A16: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| <= ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| by NORMSP_1:def 2;
abs (rseq . m) < r by A4;
then (abs (rseq . m)) * ||.((seq . m) - (lim seq)).|| < r * (p / (||.(lim seq).|| + r)) by A12, A13, A14, XREAL_1:98;
then A17: ||.((rseq . m) * ((seq . m) - (lim seq))).|| < r * (p / (||.(lim seq).|| + r)) by NORMSP_1:def 2;
||.(((rseq . m) - g1) * (lim seq)).|| = ||.(lim seq).|| * (abs ((rseq . m) - g1)) by NORMSP_1:def 2;
then A18: ||.(((rseq . m) - g1) * (lim seq)).|| <= ||.(lim seq).|| * (p / (||.(lim seq).|| + r)) by A5, A15, XREAL_1:66;
(r * (p / (||.(lim seq).|| + r))) + (||.(lim seq).|| * (p / (||.(lim seq).|| + r))) = (p / (||.(lim seq).|| + r)) * (||.(lim seq).|| + r)
.= p by A6, XCMPLX_1:88 ;
then ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| < p by A17, A18, XREAL_1:10;
hence ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p by A16, XXREAL_0:2; :: thesis: verum

end;

hence lim (rseq (#) seq) = (lim rseq) * (lim seq) by A7, NORMSP_1:def 11; :: thesis: verum