theorem :: POLYEQ_3:3

for b, c being Real
for z being Complex st b <> 0 & ( for z being Complex holds Polynom (0,b,c,z) = 0 ) holds
z = - (c / b)