( dom (id a) = a & rng (id a) = a ) by RELAT_1:45;
hence ( id a is T-Sequence-like & id a is Ordinal-yielding ) by ORDINAL1:def 7, ORDINAL2:def 4; :: thesis: verum