reconsider cs = NAT --> 0c as Complex_Sequence ;
take cs ; :: thesis: cs is constant
thus cs is constant ; :: thesis: verum