let F be domRing; :: thesis: for p being Element of the carrier of (Polynom-Ring F) st p is Unit of (Polynom-Ring F) holds
( 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) implies ( not p is zero & p is constant ) )
( p is Unit of (Polynom-Ring F) implies deg p = 0 ) by T88;
hence ( p is Unit of (Polynom-Ring F) implies ( not p is zero & p is constant ) ) by LX; :: thesis: verum