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 Element of NAT holds ||.(seq . n).|| <= M by Def10;
A3: ( z = 0 implies z * seq is bounded )

proof

assume A4: z = 0 ; :: thesis: z * seq is bounded

now

let n be Element of NAT ; :: thesis: ||.((z * seq) . n).|| <= M
||.((z * seq) . n).|| = ||.(0c * (seq . n)).|| by A4, CLVECT_1:def 15
.= ||.H₂(X).|| by CLVECT_1:2
.= 0 by CSSPACE:44 ;
hence ||.((z * seq) . n).|| <= M by A1; :: thesis: verum

end;

hence z * seq is bounded by A1, Def10; :: thesis: verum

end;

( z <> 0 implies z * seq is bounded )

proof

assume z <> 0 ; :: thesis: z * seq is bounded
then |.z.| > 0 by COMPLEX1:133;
then A5: |.z.| * M > 0 by A1, XREAL_1:131;

now

let n be Element of NAT ; :: thesis: ||.((z * seq) . n).|| <= |.z.| * M
A6: ||.((z * seq) . n).|| = ||.(z * (seq . n)).|| by CLVECT_1:def 15
.= |.z.| * ||.(seq . n).|| by CSSPACE:45 ;
|.z.| >= 0 by COMPLEX1:132;
hence ||.((z * seq) . n).|| <= |.z.| * M by A2, A6, XREAL_1:66; :: thesis: verum

end;

hence z * seq is bounded by A5, Def10; :: thesis: verum

end;

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