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 ;
A2: (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 Lm9, COMPLEX1:15 ;
A3: S₁[ 0 ] by A2;
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;
A8: (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 A6, 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 A5, A6, COMSEQ_3:def 4
.= Im (((th |^ (n + 1)) / ((n + 1) ! )) + (0 * <i> )) by A7, Def8
.= 0 by COMPLEX1:28 ;
thus S₁[n + 1] by A8; :: thesis: verum

end;

A9: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
thus for n being Nat holds (Im (Partial_Sums (th ExpSeq ))) . n = 0 by A9; :: thesis: verum

end;

A10: Im (Partial_Sums (th ExpSeq )) is constant by A1, VALUED_0:def 18;
A11: lim (Im (Partial_Sums (th ExpSeq ))) = (Im (Partial_Sums (th ExpSeq ))) . 0 by A10, SEQ_4:41
.= 0 by A1 ;
A12: Im (Sum (th ExpSeq )) = 0 by A11, COMSEQ_3:41;
A13: Sum (th ExpSeq ) = (Re (Sum (th ExpSeq ))) + (0 * <i> ) by A12, COMPLEX1:29
.= Sum (th rExpSeq ) by Th49 ;
thus Sum (th ExpSeq ) = Sum (th rExpSeq ) by A13; :: thesis: verum