let p be real number ; :: thesis: Im (Sum (p ExpSeq )) = 0
A1: for n being Element of NAT holds (Partial_Sums (Im (p ExpSeq ))) . n = 0

proof

let n be Element of NAT ; :: thesis: (Partial_Sums (Im (p ExpSeq ))) . n = 0
defpred S₁[ Element of 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 4
.= 0 by Th4, COMPLEX1:15 ;
then A2: S₁[ 0 ] ;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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 4
.= Im ((p |^ (k + 1)) / ((k + 1) !c )) by Def8
.= Im (((p |^ (k + 1)) / ((k + 1) ! )) + (0 * <i> )) by Th37
.= 0 by COMPLEX1:28 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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
( n in NAT & m in NAT ) by ORDINAL1:def 13;
then ( (Partial_Sums (Im (p ExpSeq ))) . n = 0 & (Partial_Sums (Im (p ExpSeq ))) . m = 0 ) by A1;
hence (Partial_Sums (Im (p ExpSeq ))) . n = (Partial_Sums (Im (p ExpSeq ))) . m ; :: thesis: verum

end;

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