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