set s = <*a,b*>;
A1: rng <*a,b*> = {a,b} by FINSEQ_2:147;
{a,b} c= INT

proof

( a in INT & b in INT ) by INT_1:def 2;
hence {a,b} c= INT by ZFMISC_1:38; :: thesis: verum

end;

hence <*a,b*> is FinSequence of INT by A1, FINSEQ_1:def 4; :: thesis: verum