set s = NAT --> 1;
A1: dom (NAT --> 1) = NAT by FUNCOP_1:19;
for n being Element of NAT holds (NAT --> 1) . n is real ;
then reconsider s = NAT --> 1 as Real_Sequence by A1, SEQ_1:4;
take s ; :: thesis: s is integer-yielding
let x be set ; :: according to VALUED_0:def 11 :: thesis: ( not x in dom s or s . x is integer )
assume x in dom s ; :: thesis: s . x is integer
thus s . x in INT by INT_1:def 2; :: according to INT_1:def 2 :: thesis: verum