let s, z be Complex; :: thesis: ( z ^2 = s & Im s = 0 & Re s > 0 & not z = sqrt (Re s) implies z = - (sqrt (Re s)) )
assume A1: z ^2 = s ; :: thesis: ( not Im s = 0 or not Re s > 0 or z = sqrt (Re s) or z = - (sqrt (Re s)) )
assume that
A2: Im s = 0 and
A3: Re s > 0 ; :: thesis: ( z = sqrt (Re s) or z = - (sqrt (Re s)) )
( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + (0 ^2)))) / 2))) * <i>) ) by A1, A2, Th19;
then ( z = (sqrt (((Re s) + (Re s)) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * <i>) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2))) + (- ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * <i>)) ) by A3, SQUARE_1:22;
then ( z = (sqrt (((Re s) + (Re s)) / 2)) + ((sqrt (((- (Re s)) + (Re s)) / 2)) * <i>) or z = (- (sqrt (((Re s) + (Re s)) / 2))) + (- ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * <i>)) ) by A3, SQUARE_1:22;
then ( z = (sqrt (Re s)) + ((sqrt ((0 + ((Re s) - (Re s))) / 2)) * <i>) or z = (- (sqrt (Re s))) + (- ((sqrt ((0 + ((Re s) - (Re s))) / 2)) * <i>)) ) by A3, SQUARE_1:22;
hence ( z = sqrt (Re s) or z = - (sqrt (Re s)) ) by SQUARE_1:17; :: thesis: verum