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