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