let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded
let seq be sequence of X; :: thesis: ( Rseq is bounded & seq is bounded implies Rseq * seq is bounded )
assume that
A1: Rseq is bounded and
A2: seq is bounded ; :: thesis: Rseq * seq is bounded
consider M1 being real number such that
A3: M1 > 0 and
A4: for n being Element of NAT holds abs (Rseq . n) < M1 by A1, SEQ_2:3;
consider M2 being Real such that
A5: M2 > 0 and
A6: for n being Element of NAT holds ||.(seq . n).|| <= M2 by A2, BHSP_3:def 3;

now

reconsider M = M1 * M2 as Real ;
take M = M; :: thesis: ( M > 0 & ( for n being Element of NAT holds ||.((Rseq * seq) . n).|| <= M ) )

now

let n be Element of NAT ; :: thesis: ||.((Rseq * seq) . n).|| <= M
abs (Rseq . n) >= 0 by COMPLEX1:46;
then A7: (abs (Rseq . n)) * ||.(seq . n).|| <= (abs (Rseq . n)) * M2 by A6, XREAL_1:64;
abs (Rseq . n) <= M1 by A4;
then A8: (abs (Rseq . n)) * M2 <= M1 * M2 by A5, XREAL_1:64;
||.((Rseq * seq) . n).|| = ||.((Rseq . n) * (seq . n)).|| by Def9
.= (abs (Rseq . n)) * ||.(seq . n).|| by BHSP_1:27 ;
hence ||.((Rseq * seq) . n).|| <= M by A7, A8, XXREAL_0:2; :: thesis: verum

end;

hence ( M > 0 & ( for n being Element of NAT holds ||.((Rseq * seq) . n).|| <= M ) ) by A3, A5, XREAL_1:129; :: thesis: verum

end;

hence Rseq * seq is bounded by BHSP_3:def 3; :: thesis: verum