reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
take cs ; :: thesis: cs is constant
thus cs is constant ; :: thesis: verum