let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for z being Complex st seq is absolutely_summable holds
z * seq is absolutely_summable
let seq be sequence of X; :: thesis: for z being Complex st seq is absolutely_summable holds
z * seq is absolutely_summable
let z be Complex; :: thesis: ( seq is absolutely_summable implies z * seq is absolutely_summable )
assume seq is absolutely_summable ; :: thesis: z * seq is absolutely_summable
then ||.seq.|| is summable by Def8;
then A1: |.z.| (#) ||.seq.|| is summable by SERIES_1:13;
for n being Element of NAT holds
( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n )

proof

let n be Element of NAT ; :: thesis: ( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n )
thus ||.(z * seq).|| . n >= 0 :: thesis: ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n

proof

||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def 3;
hence ||.(z * seq).|| . n >= 0 by CSSPACE:46; :: thesis: verum

end;

thus ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n :: thesis: verum

proof

||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def 3
.= ||.(z * (seq . n)).|| by CLVECT_1:def 15
.= |.z.| * ||.(seq . n).|| by CSSPACE:45
.= |.z.| * (||.seq.|| . n) by CLVECT_2:def 3
.= (|.z.| (#) ||.seq.||) . n by SEQ_1:13 ;
hence ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n ; :: thesis: verum

end;

end;

then ||.(z * seq).|| is summable by A1, SERIES_1:24;
hence z * seq is absolutely_summable by Def8; :: thesis: verum