let p, q, t, u, v be Integer; :: thesis: ( p + q divides u - v implies p + q divides (p * (u + t)) + (q * (v + t)) )
set z = u - v;
assume p + q divides u - v ; :: thesis: p + q divides (p * (u + t)) + (q * (v + t))
then p + q divides (p * (u - v)) + (q * 0) by INT_2:2;
then p + q divides (p * ((u - v) + (v + t))) + (q * (0 + (v + t))) by Th29;
hence p + q divides (p * (u + t)) + (q * (v + t)) ; :: thesis: verum