0_. L is Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;
hence not for b₁ being Element of the carrier of (Polynom-Ring L) holds b₁ is monic ; :: thesis: verum