dom <%x%> = 1 by Def5;
hence ( <%x%> is finite & <%x%> is T-Sequence-like ) by FINSET_1:29, ORDINAL1:def 7; :: thesis: verum