let F be domRing; :: thesis: for p being Polynomial of F holds
( ( p is monic & p is constant ) iff p = 1_. F )
let p be Polynomial of F; :: thesis: ( ( p is monic & p is constant ) iff p = 1_. F )
reconsider q = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

now :: thesis: ( p is monic & p is constant implies p = 1_. F )

assume B: ( p is monic & p is constant ) ; :: thesis: p = 1_. F
then H: LC q = 1. F by RATFUNC1:def 7;
deg p <= 0 by B, RATFUNC1:def 2;
then consider a being Element of F such that
A: q = a | F by RING_4:def 4, RING_4:20;
1. F = a by H, A, RING_5:6;
hence p = 1_. F by A, RING_4:14; :: thesis: verum

end;

hence ( ( p is monic & p is constant ) iff p = 1_. F ) ; :: thesis: verum