let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds 0_. F in { q where q is Polynomial of F : deg q < deg p }
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: 0_. F in { q where q is Polynomial of F : deg q < deg p }
deg (0_. F) = - 1 by HURWITZ:20;
hence 0_. F in { q where q is Polynomial of F : deg q < deg p } ; :: thesis: verum