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

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