let S be RealNormSpace; 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; 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; ( 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
; 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;
( 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
;
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;
for m being Nat st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
let m be
Nat;
( n <= m implies ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p )
assume A11:
n <= m
;
||.(((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;
verum
end;
rseq (#) seq is convergent
by A1, A2, Th13;
hence
lim (rseq (#) seq) = (lim rseq) * (lim seq)
by A7, NORMSP_1:def 7; verum