let X be RealUnitarySpace; :: thesis: for a being Real
for seq being sequence of X st seq is bounded holds
a * seq is bounded
let a be Real; :: thesis: for seq being sequence of X st seq is bounded holds
a * seq is bounded
let seq be sequence of X; :: thesis: ( seq is bounded implies a * seq is bounded )
assume seq is bounded ; :: thesis: a * seq is bounded
then consider M being Real such that
A1: M > 0 and
A2: for n being Element of NAT holds ||.(seq . n).|| <= M by Def3;
A3: ( a <> 0 implies a * seq is bounded )

proof

A4: now

let n be Element of NAT ; :: thesis: ||.((a * seq) . n).|| <= (abs a) * M
A5: abs a >= 0 by COMPLEX1:46;
||.((a * seq) . n).|| = ||.(a * (seq . n)).|| by NORMSP_1:def 5
.= (abs a) * ||.(seq . n).|| by BHSP_1:27 ;
hence ||.((a * seq) . n).|| <= (abs a) * M by A2, A5, XREAL_1:64; :: thesis: verum

end;

assume a <> 0 ; :: thesis: a * seq is bounded
then abs a > 0 by COMPLEX1:47;
then (abs a) * M > 0 by A1, XREAL_1:129;
hence a * seq is bounded by A4, Def3; :: thesis: verum

end;

( a = 0 implies a * seq is bounded )

proof

assume A6: a = 0 ; :: thesis: a * seq is bounded

now

let n be Element of NAT ; :: thesis: ||.((a * seq) . n).|| <= M
||.((a * seq) . n).|| = ||.(0 * (seq . n)).|| by A6, NORMSP_1:def 5
.= ||.H₁(X).|| by RLVECT_1:10
.= 0 by BHSP_1:26 ;
hence ||.((a * seq) . n).|| <= M by A1; :: thesis: verum

end;

hence a * seq is bounded by A1, Def3; :: thesis: verum

end;

hence a * seq is bounded by A3; :: thesis: verum