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