set s = <*a*>;
A1: rng <*a*> = {a} by FINSEQ_1:55;
a in INT by INT_1:def 2;
then {a} c= INT by ZFMISC_1:37;
hence <*a*> is FinSequence of INT by A1, FINSEQ_1:def 4; :: thesis: verum