let F be Field; :: thesis: 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
let r, q, u be Polynomial of F; :: thesis: for p being non zero Polynomial of F holds (((r *' q) mod p) *' u) mod p = ((r *' q) *' u) mod p
let p be non zero Polynomial of F; :: thesis: (((r *' q) mod p) *' u) mod p = ((r *' q) *' u) mod p
A: (((r *' q) mod p) *' u) mod p = (((r *' q) *' u) + ((- (((r *' q) div p) *' p)) *' u)) mod p by POLYNOM3:32
.= (((r *' q) *' u) mod p) + (((- (((r *' q) div p) *' p)) *' u) mod p) by div4 ;
(- (((r *' q) div p) *' p)) *' u = (p *' (- ((r *' q) div p))) *' u by HURWITZ:12
.= p *' ((- ((r *' q) div p)) *' u) by POLYNOM3:33 ;
hence (((r *' q) mod p) *' u) mod p = (((r *' q) *' u) mod p) + (0_. F) by A, div2, T2
.= ((r *' q) *' u) mod p by POLYNOM3:28 ;
:: thesis: verum