set s = NAT --> 1;
A1: dom (NAT --> 1) = NAT by FUNCOP_1:13;
for n being Nat holds (NAT --> 1) . n is real ;
then reconsider s = NAT --> 1 as Real_Sequence by SEQ_1:2, A1;
take s ; :: thesis: s is INT -valued
thus s is INT -valued ; :: thesis: verum