let seq be Complex_Sequence; :: thesis: ( seq is summable implies Sum (seq *' ) = (Sum seq) *' )
assume seq is summable ; :: thesis: Sum (seq *' ) = (Sum seq) *'
then A1: Partial_Sums seq is convergent ;
Sum (seq *' ) = lim (Partial_Sums (seq *' )) by COMSEQ_3:def 8
.= lim ((Partial_Sums seq) *' ) by Lm2
.= (lim (Partial_Sums seq)) *' by A1, COMSEQ_2:12 ;
hence Sum (seq *' ) = (Sum seq) *' by COMSEQ_3:def 8; :: thesis: verum