NAT --> 0 is sequence of COMPLEX by XCMPLX_0:def 2, FUNCOP_1:45;
hence ex b₁ being Complex_Sequence st b₁ is empty-yielding ; :: thesis: verum