let Rseq be Real_Sequence; for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
let X be RealUnitarySpace; for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
let seq be sequence of X; ( Rseq is convergent & seq is convergent implies ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) ) )
assume that
A1:
Rseq is convergent
and
A2:
seq is convergent
; ( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
consider b being Real such that
A3:
b > 0
and
A4:
for n being Nat holds |.(Rseq . n).| < b
by A1, SEQ_2:3, SEQ_2:13;
reconsider b = b as Real ;
A5:
b + ||.(lim seq).|| > 0 + 0
by A3, BHSP_1:28, XREAL_1:8;
A6:
||.(lim seq).|| >= 0
by BHSP_1:28;
A7:
now for r being Real st r > 0 holds
ex m being set st
for n being Nat st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < rlet r be
Real;
( r > 0 implies ex m being set st
for n being Nat st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r )assume
r > 0
;
ex m being set st
for n being Nat st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < rthen A8:
r / (b + ||.(lim seq).||) > 0
by A5, XREAL_1:139;
then consider m1 being
Nat such that A9:
for
n being
Nat st
n >= m1 holds
|.((Rseq . n) - (lim Rseq)).| < r / (b + ||.(lim seq).||)
by A1, SEQ_2:def 7;
consider m2 being
Nat such that A10:
for
n being
Nat st
n >= m2 holds
dist (
(seq . n),
(lim seq))
< r / (b + ||.(lim seq).||)
by A2, A8, BHSP_2:def 2;
take m =
m1 + m2;
for n being Nat st n >= m holds
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < rlet n be
Nat;
( n >= m implies dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r )assume A11:
n >= m
;
dist (((Rseq * seq) . n),((lim Rseq) * (lim seq))) < r
m1 + m2 >= m1
by NAT_1:12;
then
n >= m1
by A11, XXREAL_0:2;
then
|.((Rseq . n) - (lim Rseq)).| <= r / (b + ||.(lim seq).||)
by A9;
then A12:
||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).| <= ||.(lim seq).|| * (r / (b + ||.(lim seq).||))
by A6, XREAL_1:64;
A13:
||.((seq . n) - (lim seq)).|| >= 0
by BHSP_1:28;
m >= m2
by NAT_1:12;
then
n >= m2
by A11, XXREAL_0:2;
then
dist (
(seq . n),
(lim seq))
< r / (b + ||.(lim seq).||)
by A10;
then A14:
||.((seq . n) - (lim seq)).|| < r / (b + ||.(lim seq).||)
by BHSP_1:def 5;
(
|.(Rseq . n).| < b &
|.(Rseq . n).| >= 0 )
by A4, COMPLEX1:46;
then
|.(Rseq . n).| * ||.((seq . n) - (lim seq)).|| < b * (r / (b + ||.(lim seq).||))
by A14, A13, XREAL_1:96;
then
(|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).|) < (b * (r / (b + ||.(lim seq).||))) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||)))
by A12, XREAL_1:8;
then
(|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||)))
by XCMPLX_1:74;
then
(|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + ((||.(lim seq).|| * r) / (b + ||.(lim seq).||))
by XCMPLX_1:74;
then
(|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).|) < ((b * r) + (||.(lim seq).|| * r)) / (b + ||.(lim seq).||)
by XCMPLX_1:62;
then
(|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).|) < ((b + ||.(lim seq).||) * r) / (b + ||.(lim seq).||)
;
then A15:
(|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).|) < r
by A5, XCMPLX_1:89;
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| =
||.(((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))).||
by Def7
.=
||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + H1(X)).||
.=
||.((((Rseq . n) * (seq . n)) - ((lim Rseq) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq)))).||
by RLVECT_1:15
.=
||.(((Rseq . n) * (seq . n)) - (((lim Rseq) * (lim seq)) - (((Rseq . n) * (lim seq)) - ((Rseq . n) * (lim seq))))).||
by RLVECT_1:29
.=
||.(((Rseq . n) * (seq . n)) - (((Rseq . n) * (lim seq)) + (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq))))).||
by RLVECT_1:29
.=
||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) - (((lim Rseq) * (lim seq)) - ((Rseq . n) * (lim seq)))).||
by RLVECT_1:27
.=
||.((((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))) + (((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq)))).||
by RLVECT_1:33
;
then
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.(((Rseq . n) * (seq . n)) - ((Rseq . n) * (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).||
by BHSP_1:30;
then
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) * (lim seq)) - ((lim Rseq) * (lim seq))).||
by RLVECT_1:34;
then
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= ||.((Rseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).||
by RLVECT_1:35;
then
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= (|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + ||.(((Rseq . n) - (lim Rseq)) * (lim seq)).||
by BHSP_1:27;
then
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| <= (|.(Rseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Rseq . n) - (lim Rseq)).|)
by BHSP_1:27;
then
||.(((Rseq * seq) . n) - ((lim Rseq) * (lim seq))).|| < r
by A15, XXREAL_0:2;
hence
dist (
((Rseq * seq) . n),
((lim Rseq) * (lim seq)))
< r
by BHSP_1:def 5;
verum end;
Rseq * seq is convergent
by A1, A2, Th48;
hence
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
by A7, BHSP_2:def 2; verum