let X be Complex_Banach_Algebra; :: thesis: for z being Element of X holds 1 <= Sum (||.z.|| rExpSeq )
let z be Element of X; :: thesis: 1 <= Sum (||.z.|| rExpSeq )
||.((Partial_Sums (z ExpSeq )) . 0 ).|| = ||.((z ExpSeq ) . 0 ).|| by BHSP_4:def 1
.= ||.(1. X).|| by Th13
.= 1 by CLOPBAN3:42 ;
hence 1 <= Sum (||.z.|| rExpSeq ) by Th27; :: thesis: verum