let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds
( p is Unit of (Polynom-Ring F) iff ( not p is zero & p is constant ) )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( p is Unit of (Polynom-Ring F) iff ( not p is zero & p is constant ) )
( p is Unit of (Polynom-Ring F) iff deg p = 0 ) by T8;
hence ( p is Unit of (Polynom-Ring F) iff ( not p is zero & p is constant ) ) by LX; :: thesis: verum