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