theorem Lm37: :: ALGNUM_1:30

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)