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