let th be Real; :: thesis: Sum (th ExpSeq) = Sum (th rExpSeq)
A1: for n being Nat holds (Im (Partial_Sums (th ExpSeq))) . n = In (0,REAL)

proof

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

proof

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

end;

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

end;

then Im (Partial_Sums (th ExpSeq)) is constant by VALUED_0:def 18;
then lim (Im (Partial_Sums (th ExpSeq))) = (Im (Partial_Sums (th ExpSeq))) . 0 by SEQ_4:26
.= 0 by A1 ;
then Im (Sum (th ExpSeq)) = 0 by COMSEQ_3:41;
then Sum (th ExpSeq) = (Re (Sum (th ExpSeq))) + (0 * <i>) by COMPLEX1:13
.= Sum (th rExpSeq) by Th44 ;
hence Sum (th ExpSeq) = Sum (th rExpSeq) ; :: thesis: verum