for u being set st u in {i} holds
u in INT by INT_1:def 2;
then A1: {i} c= INT by TARSKI:def 3;
rng <*i*> = {i} by FINSEQ_1:56;
hence <*i*> is integer-yielding by A1, VALUED_0:def 5; :: thesis: verum