reconsider s = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
take s ; :: thesis: s is rational-valued
let n be Element of NAT ; :: according to PREPOWER:def 5 :: thesis: s . n is Rational
thus s . n is Rational ; :: thesis: verum