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