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