let p be Real; :: thesis: Im (Sum (p ExpSeq)) = 0
A1: for n being Nat holds (Partial_Sums (Im (p ExpSeq))) . n = 0

proof

let n be Nat; :: thesis: (Partial_Sums (Im (p ExpSeq))) . n = 0
defpred S₁[ Nat] means (Partial_Sums (Im (p ExpSeq))) . $1 = 0 ;
(Partial_Sums (Im (p ExpSeq))) . 0 = (Im (p ExpSeq)) . 0 by SERIES_1:def 1
.= Im ((p ExpSeq) . 0) by COMSEQ_3:def 6
.= 0 by Th3, COMPLEX1:6 ;
then A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume (Partial_Sums (Im (p ExpSeq))) . k = 0 ; :: thesis: S₁[k + 1]
then (Partial_Sums (Im (p ExpSeq))) . (k + 1) = 0 + ((Im (p ExpSeq)) . (k + 1)) by SERIES_1:def 1
.= Im ((p ExpSeq) . (k + 1)) by COMSEQ_3:def 6
.= Im ((p |^ (k + 1)) / ((k + 1) !)) by Def4
.= Im (((p |^ (k + 1)) / ((k + 1) !)) + (0 * <i>))
.= 0 by COMPLEX1:12 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence (Partial_Sums (Im (p ExpSeq))) . n = 0 ; :: thesis: verum

end;

for n, m being Nat holds (Partial_Sums (Im (p ExpSeq))) . n = (Partial_Sums (Im (p ExpSeq))) . m

proof

let n, m be Nat; :: thesis: (Partial_Sums (Im (p ExpSeq))) . n = (Partial_Sums (Im (p ExpSeq))) . m
( m in NAT & (Partial_Sums (Im (p ExpSeq))) . n = 0 ) by A1, ORDINAL1:def 12;
hence (Partial_Sums (Im (p ExpSeq))) . n = (Partial_Sums (Im (p ExpSeq))) . m by A1; :: thesis: verum

end;

then A4: lim (Partial_Sums (Im (p ExpSeq))) = (Partial_Sums (Im (p ExpSeq))) . 0 by SEQ_4:26, VALUED_0:24
.= 0 by A1 ;
Im (Sum (p ExpSeq)) = Im ((Sum (Re (p ExpSeq))) + ((Sum (Im (p ExpSeq))) * <i>)) by COMSEQ_3:53
.= Sum (Im (p ExpSeq)) by COMPLEX1:12 ;
hence Im (Sum (p ExpSeq)) = 0 by A4, SERIES_1:def 3; :: thesis: verum