let X be 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 rExpSeq)) . 0).|| = ||.((z rExpSeq) . 0).|| by BHSP_4:def 1
.= ||.(1. X).|| by Th14
.= 1 by LOPBAN_3:38 ;
hence 1 <= Sum (||.z.|| rExpSeq) by Th28; :: thesis: verum