let X be RealNormSpace; :: thesis: for seq being summable sequence of X
for z being Real holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let seq be summable sequence of X; :: thesis: for z being Real holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let z be Real; :: thesis: ( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
A1: Partial_Sums (z * seq) = z * (Partial_Sums seq) by Th24;
A2: Partial_Sums seq is convergent by Def2;
then A3: z * (Partial_Sums seq) is convergent by NORMSP_1:37;
Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th24
.= z * (Sum seq) by A2, NORMSP_1:45 ;
hence ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) by A3, A1, Def2; :: thesis: verum