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