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 6
.= Im ((th ExpSeq ) . 0 ) by SERIES_1:def 1
.= 0 by Lm9, COMPLEX1:15 ;
then A3: S₁[ 0 ] ;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: (Im (Partial_Sums (th ExpSeq ))) . n = 0 ; :: thesis: S₁[n + 1]
A6: n in NAT by ORDINAL1:def 13;
A7: (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 6
.= Im (((Partial_Sums (th ExpSeq )) . n) + ((th ExpSeq ) . (n + 1))) by A6, SERIES_1:def 1
.= (Im ((Partial_Sums (th ExpSeq )) . n)) + (Im ((th ExpSeq ) . (n + 1))) by COMPLEX1:19
.= 0 + (Im ((th ExpSeq ) . (n + 1))) by A5, A6, COMSEQ_3:def 6
.= Im (((th |^ (n + 1)) / ((n + 1) ! )) + (0 * <i> )) by A7, Def8
.= 0 by COMPLEX1:28 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
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 Im (Sum (th ExpSeq )) = 0 by COMSEQ_3:41;
then Sum (th ExpSeq ) = (Re (Sum (th ExpSeq ))) + (0 * <i> ) by COMPLEX1:29
.= Sum (th rExpSeq ) by Th49 ;
hence Sum (th ExpSeq ) = Sum (th rExpSeq ) ; :: thesis: verum