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 ;
A2: (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 ;
A3: S₁[ 0 ] by A2;
A4: 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 A5: (Partial_Sums (Im (p ExpSeq ))) . k = 0 ; :: thesis: S₁[k + 1]
A6: (Partial_Sums (Im (p ExpSeq ))) . (k + 1) = 0 + ((Im (p ExpSeq )) . (k + 1)) by A5, 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 ;
thus S₁[k + 1] by A6; :: thesis: verum

end;

A7: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
thus (Partial_Sums (Im (p ExpSeq ))) . n = 0 by A7; :: thesis: verum

end;

A8: 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
A9: n in NAT by ORDINAL1:def 13;
A10: ( m in NAT & (Partial_Sums (Im (p ExpSeq ))) . n = 0 ) by A1, A9, ORDINAL1:def 13;
thus (Partial_Sums (Im (p ExpSeq ))) . n = (Partial_Sums (Im (p ExpSeq ))) . m by A1, A10; :: thesis: verum

end;

A11: lim (Partial_Sums (Im (p ExpSeq ))) = (Partial_Sums (Im (p ExpSeq ))) . 0 by A8, SEQ_4:41, VALUED_0:24
.= 0 by A1 ;
A12: 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 ;
thus Im (Sum (p ExpSeq )) = 0 by A11, A12, SERIES_1:def 3; :: thesis: verum