reconsider s = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
take s ; :: thesis: s is RAT -valued
thus s is RAT -valued ; :: thesis: verum