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]

let n be Nat; :: thesis:
assume A4: (Im (Partial_Sums (th ExpSeq))) . n = 0 ; :: thesis:
(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:

end;

end;