let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds
Cseq * seq is bounded
let seq be sequence of X; :: thesis: for Cseq being Complex_Sequence st Cseq is bounded & seq is bounded holds
Cseq * seq is bounded
let Cseq be Complex_Sequence; :: thesis: ( Cseq is bounded & seq is bounded implies Cseq * seq is bounded )
assume that
A1: Cseq is bounded and
A2: seq is bounded ; :: thesis: Cseq * seq is bounded
consider M1 being Real such that
A3: M1 > 0 and
A4: for n being Nat holds |.(Cseq . n).| < M1 by A1, COMSEQ_2:8;
consider M2 being Real such that
A5: M2 > 0 and
A6: for n being Nat holds ||.(seq . n).|| <= M2 by A2, CLVECT_2:def 10;
now :: thesis: ex M being set st
( M > 0 & ( for n being Nat holds ||.((Cseq * seq) . n).|| <= M ) )
set M = M1 * M2;
take M = M1 * M2; :: thesis: ( M > 0 & ( for n being Nat holds ||.((Cseq * seq) . n).|| <= M ) )
now :: thesis: for n being Nat holds ||.((Cseq * seq) . n).|| <= M
let n be Nat; :: thesis: ||.((Cseq * seq) . n).|| <= M
|.(Cseq . n).| >= 0 by COMPLEX1:46;
then A7: |.(Cseq . n).| * ||.(seq . n).|| <= |.(Cseq . n).| * M2 by A6, XREAL_1:64;
|.(Cseq . n).| <= M1 by A4;
then A8: |.(Cseq . n).| * M2 <= M1 * M2 by A5, XREAL_1:64;
||.((Cseq * seq) . n).|| = ||.((Cseq . n) * (seq . n)).|| by Def8
.= |.(Cseq . n).| * ||.(seq . n).|| by CSSPACE:43 ;
hence ||.((Cseq * seq) . n).|| <= M by A7, A8, XXREAL_0:2; :: thesis: verum
end;
hence ( M > 0 & ( for n being Nat holds ||.((Cseq * seq) . n).|| <= M ) ) by A3, A5; :: thesis: verum
end;
hence Cseq * seq is bounded by CLVECT_2:def 10; :: thesis: verum