let x, y be Surreal; ( 0_No <= x & x == y * y & not y == sqrt x implies y == - (sqrt x) )
set s = sqrt x;
assume A1:
( 0_No <= x & x == y * y )
; ( y == sqrt x or y == - (sqrt x) )
then A2:
(sqrt x) * (sqrt x) == x
by Th19;
( ((sqrt x) + (- y)) * (sqrt x) == ((sqrt x) * (sqrt x)) + ((- y) * (sqrt x)) & ((sqrt x) + (- y)) * y == ((sqrt x) * y) + ((- y) * y) )
by SURREALR:67;
then
( ((sqrt x) + (- y)) * ((sqrt x) + y) == (((sqrt x) + (- y)) * (sqrt x)) + (((sqrt x) + (- y)) * y) & (((sqrt x) + (- y)) * (sqrt x)) + (((sqrt x) + (- y)) * y) == (((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y)) )
by SURREALR:67, SURREALR:66;
then A3:
((sqrt x) + (- y)) * ((sqrt x) + y) == (((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y))
by SURREALO:4;
( ((- y) * (sqrt x)) + ((sqrt x) * y) == (- ((sqrt x) * y)) + ((sqrt x) * y) & (- ((sqrt x) * y)) + ((sqrt x) * y) = ((sqrt x) * y) - ((sqrt x) * y) & ((sqrt x) * y) - ((sqrt x) * y) == 0_No )
by SURREALR:39, SURREALR:58;
then A4:
((- y) * (sqrt x)) + ((sqrt x) * y) == 0_No
by SURREALO:4;
A5:
((sqrt x) * (sqrt x)) + ((- y) * y) == ((sqrt x) * (sqrt x)) + (- (y * y))
by SURREALR:58;
A6:
- (y * y) == - x
by A1, SURREALR:65;
(((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y)) =
((sqrt x) * (sqrt x)) + (((- y) * (sqrt x)) + (((sqrt x) * y) + ((- y) * y)))
by SURREALR:37
.=
((sqrt x) * (sqrt x)) + ((((- y) * (sqrt x)) + ((sqrt x) * y)) + ((- y) * y))
by SURREALR:37
.=
(((sqrt x) * (sqrt x)) + ((- y) * y)) + (((- y) * (sqrt x)) + ((sqrt x) * y))
by SURREALR:37
;
then
(((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y)) == (((sqrt x) * (sqrt x)) + (- (y * y))) + 0_No
by A4, A5, SURREALR:66;
then
( ((sqrt x) + (- y)) * ((sqrt x) + y) == ((sqrt x) * (sqrt x)) + (- (y * y)) & ((sqrt x) * (sqrt x)) + (- (y * y)) == x - x )
by SURREALR:66, A3, A6, SURREALO:4, A2;
then
( ((sqrt x) + (- y)) * ((sqrt x) + y) == x - x & x - x == 0_No )
by SURREALO:4, SURREALR:39;
then
((sqrt x) + (- y)) * ((sqrt x) + y) == 0_No
by SURREALO:4;
then
( (sqrt x) - y == 0_No or (sqrt x) - (- y) == 0_No )
by SURREALR:72, SURREALR:74;
then
( sqrt x == y or sqrt x == - y )
by SURREALR:47;
then
( sqrt x == y or - (sqrt x) == - (- y) )
by SURREALR:10;
hence
( y == sqrt x or y == - (sqrt x) )
; verum