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 integer-yielding
let x be set ; :: according to VALUED_0:def 11 :: thesis: ( not x in proj1 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