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