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