let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
Cseq * seq is convergent
let seq be sequence of X; :: thesis: for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
Cseq * seq is convergent
let Cseq be Complex_Sequence; :: thesis: ( Cseq is convergent & seq is convergent implies Cseq * seq is convergent )
assume that
A1: Cseq is convergent and
A2: seq is convergent ; :: thesis: Cseq * seq is convergent
consider p being Complex such that
A3: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
|.((Cseq . n) - p).| < r by A1, COMSEQ_2:def 5;
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, CLVECT_2:9;
now :: thesis: ex h being Element of the U1 of X st
for r being Real st r > 0 holds
ex m being set st
for n being Nat st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
take h = p * g; :: thesis: for r being Real st r > 0 holds
ex m being set st
for n being Nat st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
let r be Real; :: thesis: ( r > 0 implies ex m being set st
for n being Nat st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r )
Cseq is bounded by A1;
then consider b being Real such that
A5: b > 0 and
A6: for n being Nat holds |.(Cseq . n).| < b by COMSEQ_2:8;
A7: b + ||.g.|| > 0 + 0 by A5, CSSPACE:44, XREAL_1:8;
assume A8: r > 0 ; :: thesis: ex m being set st
for n being Nat st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
then consider m1 being Nat such that
A9: for n being Nat st n >= m1 holds
|.((Cseq . n) - p).| < r / (b + ||.g.||) by A3, A7;
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;
take m = m1 + m2; :: thesis: for n being Nat st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
let n be Nat; :: thesis: ( n >= m implies ||.(((Cseq * seq) . n) - h).|| < r )
assume A11: n >= m ; :: thesis: ||.(((Cseq * seq) . n) - h).|| < r
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A11, XXREAL_0:2;
then ( ||.g.|| >= 0 & |.((Cseq . n) - p).| <= r / (b + ||.g.||) ) by A9, CSSPACE:44;
then A12: ||.g.|| * |.((Cseq . n) - p).| <= ||.g.|| * (r / (b + ||.g.||)) by XREAL_1:64;
A13: ( |.(Cseq . n).| >= 0 & ||.((seq . n) - g).|| >= 0 ) by COMPLEX1:46, CSSPACE:44;
m >= m2 by NAT_1:12;
then n >= m2 by A11, XXREAL_0:2;
then A14: ||.((seq . n) - g).|| < r / (b + ||.g.||) by A10;
|.(Cseq . n).| < b by A6;
then |.(Cseq . n).| * ||.((seq . n) - g).|| < b * (r / (b + ||.g.||)) by A14, A13, XREAL_1:96;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < (b * (r / (b + ||.g.||))) + (||.g.|| * (r / (b + ||.g.||))) by A12, XREAL_1:8;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + (||.g.|| * (r / (b + ||.g.||))) by XCMPLX_1:74;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + ((||.g.|| * r) / (b + ||.g.||)) by XCMPLX_1:74;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) + (||.g.|| * r)) / (b + ||.g.||) by XCMPLX_1:62;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b + ||.g.||) * r) / (b + ||.g.||) ;
then A15: (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < r by A7, XCMPLX_1:89;
||.(((Cseq * seq) . n) - (p * g)).|| = ||.(((Cseq . n) * (seq . n)) - (p * g)).|| by Def8
.= ||.((((Cseq . n) * (seq . n)) - (p * g)) + H1(X)).|| by RLVECT_1:4
.= ||.((((Cseq . n) * (seq . n)) - (p * g)) + (((Cseq . n) * g) - ((Cseq . n) * g))).|| by RLVECT_1:15
.= ||.(((Cseq . n) * (seq . n)) - ((p * g) - (((Cseq . n) * g) - ((Cseq . n) * g)))).|| by RLVECT_1:29
.= ||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * g) + ((p * g) - ((Cseq . n) * g)))).|| by RLVECT_1:29
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) - ((p * g) - ((Cseq . n) * g))).|| by RLVECT_1:27
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) + (((Cseq . n) * g) - (p * g))).|| by RLVECT_1:33 ;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CSSPACE:46;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CLVECT_1:9;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) - p) * g).|| by CLVECT_1:10;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + ||.(((Cseq . n) - p) * g).|| by CSSPACE:43;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) by CSSPACE:43;
hence ||.(((Cseq * seq) . n) - h).|| < r by A15, XXREAL_0:2; :: thesis: verum
end;
hence Cseq * seq is convergent by CLVECT_2:9; :: thesis: verum