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