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