let seq be Complex_Sequence; :: thesis: ( seq is summable implies Sum (seq *') = (Sum seq) *' )

assume A1: seq is summable ; :: thesis: Sum (seq *') = (Sum seq) *'

Sum (seq *') = lim (Partial_Sums (seq *')) by COMSEQ_3:def 7

.= lim ((Partial_Sums seq) *') by Lm1

.= (lim (Partial_Sums seq)) *' by A1, COMSEQ_2:12 ;

hence Sum (seq *') = (Sum seq) *' by COMSEQ_3:def 7; :: thesis: verum

assume A1: seq is summable ; :: thesis: Sum (seq *') = (Sum seq) *'

Sum (seq *') = lim (Partial_Sums (seq *')) by COMSEQ_3:def 7

.= lim ((Partial_Sums seq) *') by Lm1

.= (lim (Partial_Sums seq)) *' by A1, COMSEQ_2:12 ;

hence Sum (seq *') = (Sum seq) *' by COMSEQ_3:def 7; :: thesis: verum