1_. L is Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;
hence ex b₁ being Element of the carrier of (Polynom-Ring L) st b₁ is monic ; :: thesis: verum