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;