Re (Sequel (<%> COMPLEX)) is summable ;
hence ex b₁ being real-valued Complex_Sequence st b₁ is summable ; :: thesis: verum