let F be Field; :: thesis: for p, q being Polynomial of F st q divides p holds
(p div q) *' q = p
let p, q be Polynomial of F; :: thesis: ( q divides p implies (p div q) *' q = p )
assume q divides p ; :: thesis: (p div q) *' q = p
then consider r being Polynomial of F such that
A2: q *' r = p by T2;

per cases ( q = 0_. F or q <> 0_. F ) ;

suppose A3: q = 0_. F ; :: thesis: (p div q) *' q = p

thus (p div q) *' q = 0_. F by A3, POLYNOM3:34
.= p by A2, A3, POLYNOM3:34 ; :: thesis: verum

end;

suppose A3: q <> 0_. F ; :: thesis: (p div q) *' q = p

A4: p = (q *' r) + (0_. F) by A2, POLYNOM3:28;
deg (0_. F) = - 1 by HURWITZ:20;
then deg (0_. F) < deg q by T8b, A3;
hence (p div q) *' q = p by A2, A4, HURWITZ:def 5; :: thesis: verum

end;

end;