theorem :: POLYEQ_3:21

for s, z being Complex st z ^2 = s & Im s = 0 & Re s < 0 & not z = (sqrt (- (Re s))) * <i> holds
z = - ((sqrt (- (Re s))) * <i>)