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 Th19;

A2: Partial_Sums seq is convergent by Def1;

then A3: z * (Partial_Sums seq) is convergent by NORMSP_1:22;

Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th19

.= z * (Sum seq) by A2, NORMSP_1:28 ;

hence ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) by A3, A1; :: thesis: verum

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 Th19;

A2: Partial_Sums seq is convergent by Def1;

then A3: z * (Partial_Sums seq) is convergent by NORMSP_1:22;

Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th19

.= z * (Sum seq) by A2, NORMSP_1:28 ;

hence ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) by A3, A1; :: thesis: verum