reconsider o = 0_. R as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
take o ; :: thesis: not o is linear
thus not o is linear by HURWITZ:20; :: thesis: verum