let a, y be Real; ( not y ^2 = a or y = sqrt a or y = - (sqrt a) )
assume A1:
y ^2 = a
; ( y = sqrt a or y = - (sqrt a) )
then A2:
a >= 0
by XREAL_1:63;
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:20, SQUARE_1:29;
hence
( y = sqrt a or y = - (sqrt a) )
; verum