let p, q, z, u, v be Integer; :: thesis: ( p + q divides (p * u) + (q * v) implies p + q divides (p * (u + z)) + (q * (v + z)) )
assume p + q divides (p * u) + (q * v) ; :: thesis: p + q divides (p * (u + z)) + (q * (v + z))
then consider t being Integer such that
A2: (p + q) * t = (p * u) + (q * v) ;
(p * (u + z)) + (q * (v + z)) = (p + q) * (t + z) by A2;
hence p + q divides (p * (u + z)) + (q * (v + z)) ; :: thesis: verum