let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds 1_. 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: 1_. F in { q where q is Polynomial of F : deg q < deg p }
A: deg p > 0 by defconst;
len (1_. F) = 1 by POLYNOM4:4;
then deg (1_. F) = 0 ;
hence 1_. F in { q where q is Polynomial of F : deg q < deg p } by A; :: thesis: verum