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