let F be Field; :: thesis: for p, q being Polynomial of F holds
( p mod q = 0_. F iff q divides p )
let p, q be Polynomial of F; :: thesis: ( p mod q = 0_. F iff q divides p )

A: now :: thesis: ( p mod q = 0_. F implies q divides p )

assume p mod q = 0_. F ; :: thesis: q divides p
then (p div q) *' q = (p - ((p div q) *' q)) + ((p div q) *' q) by POLYNOM3:28
.= p + ((- ((p div q) *' q)) + ((p div q) *' q)) by POLYNOM3:26
.= p + (((p div q) *' q) - ((p div q) *' q))
.= p + (0_. F) by POLYNOM3:29
.= p by POLYNOM3:28 ;
hence q divides p by T2; :: thesis: verum

end;

now :: thesis: ( q divides p implies p mod q = 0_. F )

assume A: q divides p ; :: thesis: p mod q = 0_. F
thus p mod q = p - p by A, div0
.= 0_. F by POLYNOM3:29 ; :: thesis: verum

end;

hence ( p mod q = 0_. F iff q divides p ) by A; :: thesis: verum