dom p = dom (p " ) by VALUED_1:def 7;
hence p " is T-Sequence-like by ORDINAL1:def 7; :: thesis: verum