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

proof

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

proof

||.(a * seq).|| . n = ||.((a * seq) . n).|| by BHSP_2:def 3;
hence ||.(a * seq).|| . n >= 0 by BHSP_1:34; :: thesis: verum

end;

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

proof

||.(a * seq).|| . n = ||.((a * seq) . n).|| by BHSP_2:def 3
.= ||.(a * (seq . n)).|| by NORMSP_1:def 8
.= (abs a) * ||.(seq . n).|| by BHSP_1:33
.= (abs a) * (||.seq.|| . n) by BHSP_2:def 3
.= ((abs a) (#) ||.seq.||) . n by SEQ_1:13 ;
hence ||.(a * seq).|| . n <= ((abs a) (#) ||.seq.||) . n ; :: thesis: verum

end;

end;

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