let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for z being Complex st seq is summable holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let seq be sequence of X; :: thesis: for z being Complex st seq is summable holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let z be Complex; :: thesis: ( seq is summable implies ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) )
assume seq is summable ; :: thesis: ( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
then A1: Partial_Sums seq is convergent ;
then z * (Partial_Sums seq) is convergent by CLVECT_2:5;
then Partial_Sums (z * seq) is convergent by Th3;
hence z * seq is summable ; :: thesis: Sum (z * seq) = z * (Sum seq)
thus Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th3
.= z * (Sum seq) by A1, CLVECT_2:15 ; :: thesis: verum