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