for u being object 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:39;
hence <*i*> is INT -valued by A1, RELAT_1:def 19; :: thesis: verum