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:134 ;
hence 1 <= Sum (|.z.| rExpSeq ) by Th17; :: thesis: verum