let y, a be Real; :: thesis: ( not y ^2 = a or y = sqrt a or y = - (sqrt a) )
assume A1: y ^2 = a ; :: thesis: ( y = sqrt a or y = - (sqrt a) )
then A2: a >= 0 by XREAL_1:65;
Polynom 1,0 ,(- a),y = 0 by A1;
then ( y = ((- 0 ) + (sqrt (delta 1,0 ,(- a)))) / (2 * 1) or y = ((- 0 ) - (sqrt (delta 1,0 ,(- a)))) / (2 * 1) ) by A2, POLYEQ_1:5;
then ( y = (sqrt (4 * a)) / 2 or y = (0 - (sqrt (4 * a))) / 2 ) ;
then ( y = ((sqrt a) * 2) / 2 or y = (- (2 * (sqrt a))) / 2 ) by A2, SQUARE_1:85, SQUARE_1:97;
hence ( y = sqrt a or y = - (sqrt a) ) ; :: thesis: verum