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