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

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