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

proof

A2: a in INT by INT_1:def 2;
A3: b in INT by INT_1:def 2;
c in INT by INT_1:def 2;
hence {a,b,c} c= INT by A2, A3, JORDAN16:2; :: thesis: verum

end;

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