set s = <*a*>;
a in INT by INT_1:def 2;
then ( rng <*a*> = {a} & {a} c= INT ) by FINSEQ_1:38, ZFMISC_1:31;
hence <*a*> is FinSequence of INT by FINSEQ_1:def 4; :: thesis: verum