for K being Field
for p being Element of (Polynom-Ring K) st p <> 0_. K holds
p is non zero Element of the carrier of (Polynom-Ring K)