let z, s be Element of COMPLEX ; :: thesis:
assume A1: z ^2 = s ; :: thesis:
assume A2: Im s < 0 ; :: thesis:
set a = Re s;
set b = Im s;
set u = Re z;
set v = Im z;
A4: ( z = (Re z) + ((Im z) * ) & s = (Re s) + ((Im s) * ) & Im s < 0 ) by A2, COMPLEX1:29;
z = (Re z) + ((Im z) * ) by COMPLEX1:29;
then A5: z ^2 = (((Re z) ^2 ) - ((Im z) ^2 )) + (((2 * (Re z)) * (Im z)) * ) ;
then A6: ( ((Re z) ^2 ) - ((Im z) ^2 ) = Re s & (2 * (Re z)) * (Im z) = Im s ) by A1, A4, COMPLEX1:163;
then A7: sqrt ((((Re z) ^2 ) + ((Im z) ^2 )) ^2 ) = sqrt (((Re s) ^2 ) + ((Im s) ^2 )) ;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:65;
then A8: ((Re z) ^2 ) + ((Im z) ^2 ) = sqrt (((Re s) ^2 ) + ((Im s) ^2 )) by A7, SQUARE_1:89;
2 * ((Re z) * (Im z)) < 0 by A1, A4, A5, COMPLEX1:163;
then (Re z) * (Im z) < 0 ;
then ( ( Re z < 0 & Im z > 0 ) or ( Re z > 0 & Im z < 0 ) ) by XREAL_1:135;
then ( ( - (Re z) = sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) & Im z = sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) ) or ( Re z = sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) & - (Im z) = sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) ) ) by A6, A8, SQUARE_1:89, SQUARE_1:90;
hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) * ) ) by COMPLEX1:29; :: thesis: