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 seq is convergent by Def2;
then A2: z * (Partial_Sums seq) is convergent by CLVECT_1:118;
A3: Partial_Sums (z * seq) = z * (Partial_Sums seq) by Th23;
Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th23
.= z * (Sum seq) by A1, CLVECT_1:124 ;
hence ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) by A2, A3, Def2; :: thesis: verum