let s, z be Complex; :: thesis: ( not z ^2 = s or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) )
set a = Re s;
set b = Im s;
set u = Re z;
set v = Im z;
A1: ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63;
z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
then A2: ( s = (Re s) + ((Im s) * <i>) & z ^2 = (((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>) ) by COMPLEX1:13;
assume A3: z ^2 = s ; :: thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) )
then A4: ((Re z) ^2) - ((Im z) ^2) = Re s by A2, COMPLEX1:77;
then sqrt ((((Re z) ^2) + ((Im z) ^2)) ^2) = sqrt (((Re s) ^2) + ((Im s) ^2)) by A3, A2;
then A5: ((Re z) ^2) + ((Im z) ^2) = sqrt (((Re s) ^2) + ((Im s) ^2)) by A1, SQUARE_1:22;

per cases ( Im s >= 0 or Im s < 0 ) ;

suppose Im s >= 0 ; :: thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) )

then ( ( Re z <= 0 & Im z <= 0 ) or ( Re z >= 0 & Im z >= 0 ) ) by A3, A2, COMPLEX1:77;
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 A4, A5, SQUARE_1:22, SQUARE_1:23;
hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) ) by COMPLEX1:13; :: thesis: verum

end;

suppose Im s < 0 ; :: thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) )

then 2 * ((Re z) * (Im z)) < 0 by A3, A2, COMPLEX1:77;
then (Re z) * (Im z) < 0 ;
then ( ( Re z < 0 & Im z > 0 ) or ( Re z > 0 & Im z < 0 ) ) by XREAL_1:133;
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 A4, A5, SQUARE_1:22, SQUARE_1:23;
hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * <i>) ) by COMPLEX1:13; :: thesis: verum

end;

end;