thus the carrier of (Polynom-Ring L) is L -polynomial-membered by POLYNOM3:def 10; :: according to RING_4:def 2 :: thesis: verum