let seq be Real_Sequence; :: thesis: ( seq ^\ 1 is summable implies ( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) ) )
assume A1: seq ^\ 1 is summable ; :: thesis: ( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) )
hence seq is summable by SERIES_1:13; :: thesis: Sum seq = (seq . 0) + (Sum (seq ^\ 1))
thus Sum seq = ((Partial_Sums seq) . 0) + (Sum (seq ^\ (1 + 0))) by A1, SERIES_1:13, SERIES_1:15
.= (seq . 0) + (Sum (seq ^\ 1)) by SERIES_1:def 1 ; :: thesis: verum