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