let X be ComplexUnitarySpace; :: thesis: for z being Complex
for seq being sequence of X st seq is bounded holds
z * seq is bounded
let z be Complex; :: thesis: for seq being sequence of X st seq is bounded holds
z * seq is bounded
let seq be sequence of X; :: thesis: ( seq is bounded implies z * seq is bounded )
assume seq is bounded ; :: thesis: z * seq is bounded
then consider M being Real such that
A1: M > 0 and
A2: for n being Nat holds ||.(seq . n).|| <= M ;
A3: ( z <> 0 implies z * seq is bounded )
proof
A4: now :: thesis: for n being Nat holds ||.((z * seq) . n).|| <= |.z.| * M
let n be Nat; :: thesis: ||.((z * seq) . n).|| <= |.z.| * M
A5: |.z.| >= 0 by COMPLEX1:46;
||.((z * seq) . n).|| = ||.(z * (seq . n)).|| by CLVECT_1:def 14
.= |.z.| * ||.(seq . n).|| by CSSPACE:43 ;
hence ||.((z * seq) . n).|| <= |.z.| * M by A2, A5, XREAL_1:64; :: thesis: verum
end;
assume z <> 0 ; :: thesis: z * seq is bounded
then |.z.| > 0 by COMPLEX1:47;
then |.z.| * M > 0 by A1, XREAL_1:129;
hence z * seq is bounded by A4; :: thesis: verum
end;
( z = 0 implies z * seq is bounded )
proof
assume A6: z = 0 ; :: thesis: z * seq is bounded
now :: thesis: for n being Nat holds ||.((z * seq) . n).|| <= M
let n be Nat; :: thesis: ||.((z * seq) . n).|| <= M
||.((z * seq) . n).|| = ||.(0c * (seq . n)).|| by A6, CLVECT_1:def 14
.= ||.H2(X).|| by CLVECT_1:1
.= 0 by CSSPACE:42 ;
hence ||.((z * seq) . n).|| <= M by A1; :: thesis: verum
end;
hence z * seq is bounded by A1; :: thesis: verum
end;
hence z * seq is bounded by A3; :: thesis: verum