theorem :: POLYEQ_5:30

for z, a0, a1, a2, a3, a4 being Complex st a4 <> 0 holds
( ((((a4 * (z |^ 4)) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = 1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) ) )