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