let z be Element of COMPLEX ; :: thesis: 1 <= Sum (|.z.| rExpSeq)
|.((Partial_Sums (z ExpSeq)) . 0).| = |.((z ExpSeq) . 0).| by SERIES_1:def 1
.= 1 by Th4, COMPLEX1:48 ;
hence 1 <= Sum (|.z.| rExpSeq) by Th17; :: thesis: verum