A13: - 1_No = [(-- (R_ 1_No)),(-- (L_ 1_No))] by SURREALR:7
.= [{},{(- 0_No)}] by SURREALR:21, SURREALR:22 ;
set S0 = sqrt_0 (- 1_No);
0_No in R_ (- 1_No) by A13, TARSKI:def 1;
then 0_No in R_ (NonNegativePart (- 1_No)) by Def1;
then A14: sqrt 0_No in R_ (sqrt_0 (- 1_No)) by Def9;
R_ (sqrt_0 (- 1_No)) c= {0_No}

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in R_ (sqrt_0 (- 1_No)) or o in {0_No} )
assume o in R_ (sqrt_0 (- 1_No)) ; :: thesis: o in {0_No}
then consider r being Surreal such that
A15: ( o = sqrt r & r in R_ (NonNegativePart (- 1_No)) ) by Def9;
r in R_ (- 1_No) by A15, Th2;
then r = 0_No by A13, TARSKI:def 1;
hence o in {0_No} by A15, TARSKI:def 1; :: thesis: verum

end;

then A16: R_ (sqrt_0 (- 1_No)) = {0_No} by A14, ZFMISC_1:33;
A17: L_ (sqrt_0 (- 1_No)) = {}

proof

assume L_ (sqrt_0 (- 1_No)) <> {} ; :: thesis: contradiction
then consider o being object such that
A18: o in L_ (sqrt_0 (- 1_No)) by XBOOLE_0:def 1;
consider l being Surreal such that
A19: ( o = sqrt l & l in L_ (NonNegativePart (- 1_No)) ) by A18, Def9;
l in L_ (- 1_No) by A19, Th2;
hence contradiction by A13; :: thesis: verum

end;

for y being Surreal st y in (L_ (NonNegativePart (- 1_No))) \/ (R_ (NonNegativePart (- 1_No))) holds
y == 0_No

proof

let y be Surreal; :: thesis: ( y in (L_ (NonNegativePart (- 1_No))) \/ (R_ (NonNegativePart (- 1_No))) implies y == 0_No )
assume y in (L_ (NonNegativePart (- 1_No))) \/ (R_ (NonNegativePart (- 1_No))) ; :: thesis: y == 0_No
then ( y in L_ (NonNegativePart (- 1_No)) or y in R_ (NonNegativePart (- 1_No)) ) by XBOOLE_0:def 3;
then ( y in L_ (- 1_No) or y in R_ (- 1_No) ) by Th2;
hence y == 0_No by A13, TARSKI:def 1; :: thesis: verum

end;

hence sqrt (- 1_No) = - 1_No by A17, Th25, A13, A16; :: thesis: verum