let z be Complex; :: thesis: 1 <= Sum (|.z.| rExpSeq)
|.((Partial_Sums (z ExpSeq)) . 0).| = |.((z ExpSeq) . 0).| by SERIES_1:def 1
.= 1 by Th3, COMPLEX1:48 ;
hence 1 <= Sum (|.z.| rExpSeq) by Th16; :: thesis: verum