let seq be Complex_Sequence; ( seq is summable implies for n being Nat holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) )
assume A1:
seq is summable
; for n being Nat holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))
then
Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>)
by Th53;
then A2:
( Re (Sum seq) = Sum (Re seq) & Im (Sum seq) = Sum (Im seq) )
by COMPLEX1:12;
let n be Nat; Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))
A3:
Sum (seq ^\ (n + 1)) = (Sum (Re (seq ^\ (n + 1)))) + ((Sum (Im (seq ^\ (n + 1)))) * <i>)
by A1, Th53;
A4: Sum (Im seq) =
((Partial_Sums (Im seq)) . n) + (Sum ((Im seq) ^\ (n + 1)))
by A1, SERIES_1:15
.=
((Im (Partial_Sums seq)) . n) + (Sum ((Im seq) ^\ (n + 1)))
by Th26
.=
((Im (Partial_Sums seq)) . n) + (Sum (Im (seq ^\ (n + 1))))
by Th23
.=
((Im (Partial_Sums seq)) . n) + (Im (Sum (seq ^\ (n + 1))))
by A3, COMPLEX1:12
.=
(Im ((Partial_Sums seq) . n)) + (Im (Sum (seq ^\ (n + 1))))
by Def6
.=
Im (((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))))
by COMPLEX1:8
;
Sum (Re seq) =
((Partial_Sums (Re seq)) . n) + (Sum ((Re seq) ^\ (n + 1)))
by A1, SERIES_1:15
.=
((Re (Partial_Sums seq)) . n) + (Sum ((Re seq) ^\ (n + 1)))
by Th26
.=
((Re (Partial_Sums seq)) . n) + (Sum (Re (seq ^\ (n + 1))))
by Th23
.=
((Re (Partial_Sums seq)) . n) + (Re (Sum (seq ^\ (n + 1))))
by A3, COMPLEX1:12
.=
(Re ((Partial_Sums seq) . n)) + (Re (Sum (seq ^\ (n + 1))))
by Def5
.=
Re (((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))))
by COMPLEX1:8
;
hence
Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))
by A2, A4, COMPLEX1:def 3; verum