theorem :: FIELD_9:14
for R being comRing
for p being Polynomial of R st deg p < 2 holds
for a being Element of R ex y, z being Element of R st eval (p,a) = y + (a * z)