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