let z be Element of COMPLEX ; :: thesis: 1 <= Sum (|.z.| rExpSeq )
A1: |.((Partial_Sums (z ExpSeq )) . 0 ).| = |.((z ExpSeq ) . 0 ).| by COMSEQ_3:def 7
.= 1 by Th4, COMPLEX1:134 ;
thus 1 <= Sum (|.z.| rExpSeq ) by A1, Th17; :: thesis: verum