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