( dom (NAT --> 0) = NAT & ( for x being set st x in NAT holds
(NAT --> 0) . x is Element of COMPLEX ) ) by XCMPLX_0:def 2;
then reconsider cseq = NAT --> 0 as sequence of COMPLEX by COMSEQ_1:1;
cseq is summable ;
hence ex b₁ being sequence of COMPLEX st b₁ is summable ; :: thesis: verum