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