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