let X be ComplexNormSpace; :: thesis: for seq being summable sequence of X
for z being Complex holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let seq be summable sequence of X; :: thesis: for z being Complex holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let z be Complex; :: thesis: ( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
A1: Partial_Sums (z * seq) = z * (Partial_Sums seq) by Th19;
A2: Partial_Sums seq is convergent by Def1;
then A3: z * (Partial_Sums seq) is convergent by CLVECT_1:116;
Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th19
.= z * (Sum seq) by A2, CLVECT_1:122 ;
hence ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) by A3, A1; :: thesis: verum