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

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 4
.= Im ((th ExpSeq ) . 0 ) by COMSEQ_3:def 7
.= 0 by Lm13, COMPLEX1:15 ;
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]
X: n in NAT by ORDINAL1:def 13;
A0: (th |^ (n + 1)) / ((n + 1) !c ) = (th |^ (n + 1)) / ((n + 1) ! ) by Th37;
(Im (Partial_Sums (th ExpSeq ))) . (n + 1) = Im ((Partial_Sums (th ExpSeq )) . (n + 1)) by COMSEQ_3:def 4
.= Im (((Partial_Sums (th ExpSeq )) . n) + ((th ExpSeq ) . (n + 1))) by X, COMSEQ_3:def 7
.= (Im ((Partial_Sums (th ExpSeq )) . n)) + (Im ((th ExpSeq ) . (n + 1))) by COMPLEX1:19
.= 0 + (Im ((th ExpSeq ) . (n + 1))) by A4, X, COMSEQ_3:def 4
.= Im (((th |^ (n + 1)) / ((n + 1) ! )) + (0 * <i> )) by A0, Def8
.= 0 by COMPLEX1:28 ;
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 = 0 ; :: 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:41
.= 0 by A1 ;
then A5: Im (Sum (th ExpSeq )) = 0 by COMSEQ_3:41;
Sum (th ExpSeq ) = (Re (Sum (th ExpSeq ))) + (0 * <i> ) by A5, COMPLEX1:29
.= Sum (th rExpSeq ) by Th49 ;
hence Sum (th ExpSeq ) = Sum (th rExpSeq ) ; :: thesis: verum