for F being Field
for r, q, u being Polynomial of F
for p being non zero Polynomial of F holds (((r *' q) mod p) *' u) mod p = ((r *' q) *' u) mod p