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 )
A1: for n being Nat holds
( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n )

proof

let n be Nat; :: thesis: ( ||.(z * seq).|| . n >= 0 & ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n )
||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def 3;
hence ||.(z * seq).|| . n >= 0 by CSSPACE:44; :: thesis: ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n
||.(z * seq).|| . n = ||.((z * seq) . n).|| by CLVECT_2:def 3
.= ||.(z * (seq . n)).|| by CLVECT_1:def 14
.= |.z.| * ||.(seq . n).|| by CSSPACE:43
.= |.z.| * (||.seq.|| . n) by CLVECT_2:def 3
.= (|.z.| (#) ||.seq.||) . n by SEQ_1:9 ;
hence ||.(z * seq).|| . n <= (|.z.| (#) ||.seq.||) . n ; :: thesis: verum

end;

assume seq is absolutely_summable ; :: thesis: z * seq is absolutely_summable
then ||.seq.|| is summable ;
then |.z.| (#) ||.seq.|| is summable by SERIES_1:10;
then ||.(z * seq).|| is summable by A1, SERIES_1:20;
hence z * seq is absolutely_summable ; :: thesis: verum