NAT --> 0 is sequence of COMPLEX by XCMPLX_0:def 2, FUNCOP_1:45;
hence ex b₁ being Complex_Sequence st
( b₁ is constant & b₁ is real-valued ) ; :: thesis: verum