reconsider i1 = i as Element of INT by INT_1:def 2;
<*i1*> is FinSequence of INT ;
hence <*i*> is FinSequence of INT ; :: thesis: verum