theorem :: POLYEQ_3:30

for z, z1, z2, z3 being Complex st z1 <> 0 & Polynom (z1,z2,z3,0,z) = 0 holds
for s, h, t being Complex st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * <i>)) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * <i>)) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * <i>)) - t holds
z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * <i>)) - t