consider M being Real such that
A1: M > 0 and
A2: for n being Nat holds ||.(seq . n).|| <= M by Def3;
A3: ( a <> 0 implies a * seq is bounded )
proof
A4: now :: thesis: for n being Nat holds ||.((a * seq) . n).|| <= |.a.| * M
let n be Nat; :: thesis: ||.((a * seq) . n).|| <= |.a.| * M
A5: |.a.| >= 0 by COMPLEX1:46;
||.((a * seq) . n).|| = ||.(a * (seq . n)).|| by NORMSP_1:def 5
.= |.a.| * ||.(seq . n).|| by BHSP_1:27 ;
hence ||.((a * seq) . n).|| <= |.a.| * M by A2, A5, XREAL_1:64; :: thesis: verum
end;
assume a <> 0 ; :: thesis: a * seq is bounded
then |.a.| > 0 by COMPLEX1:47;
then |.a.| * M > 0 by A1, XREAL_1:129;
hence a * seq is bounded by A4; :: thesis: verum
end;
( a = 0 implies a * seq is bounded )
proof
assume A6: a = 0 ; :: thesis: a * seq is bounded
now :: thesis: for n being Nat holds ||.((a * seq) . n).|| <= M
let n be Nat; :: thesis: ||.((a * seq) . n).|| <= M
||.((a * seq) . n).|| = ||.(0 * (seq . n)).|| by A6, NORMSP_1:def 5
.= ||.H1(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; :: thesis: verum
end;
hence a * seq is bounded by A3; :: thesis: verum