let x be Surreal; :: thesis:
set A = born x;
set Nx = NonNegativePart x;
consider S being c=-monotone Function-yielding Sequence such that
A1: ( dom S = succ (born x) & No_sqrt_op (born x) = S . (born x) ) and
A2: for B being Ordinal st B in succ (born x) holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for o being object st o in Day B holds
SB . o = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o)))] ) ) by Def6;
set UA = union (rng (S | (born x)));
consider SB being ManySortedSet of Day (born x) such that
A3: S . (born x) = SB and
A4: for o being object st o in Day (born x) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart o)))],o)))] by A2, ORDINAL1:6;
x in Day (born x) by SURREAL0:def 18;
then A5: sqrt x = [(Union (sqrtL ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart x))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart x))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart x)))],x)))] by A4, A1, A3;
A6: (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) c= L_ (sqrt_0 x)

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: y in (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) ; :: thesis:
consider o being object such that
A8: ( o in dom (union (rng (S | (born x)))) & o in L_ (NonNegativePart x) & (union (rng (S | (born x)))) . o = y ) by A7, FUNCT_1:def 6;
reconsider o = o as Surreal by SURREAL0:def 16, A8;
set b = born o;
A9: o in L_ x by Th2, A8;
A10: o in Day (born o) by SURREAL0:def 18;
A11: o in (L_ x) \/ (R_ x) by A9, XBOOLE_0:def 3;
then A12: born o in born x by SURREALO:1;
A13: born o in succ (born x) by A11, SURREALO:1, ORDINAL1:8;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A14: o in dom (S . (born o)) by A10, PARTFUN1:def 2;
then A15: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A12, SURREALR:5;
A16: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A13;
y = sqrt o by A8, A15, A13, A1, A14, SURREALR:2, A16;
hence y in L_ (sqrt_0 x) by Def9, A8; :: thesis:

end;

A17: L_ (sqrt_0 x) c= (union (rng (S | (born x)))) .: (L_ (NonNegativePart x))

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in L_ (sqrt_0 x) ; :: thesis:
then consider o being Surreal such that
A18: ( y = sqrt o & o in L_ (NonNegativePart x) ) by Def9;
set b = born o;
A19: o in L_ x by Th2, A18;
A20: o in Day (born o) by SURREAL0:def 18;
A21: o in (L_ x) \/ (R_ x) by A19, XBOOLE_0:def 3;
then A22: born o in born x by SURREALO:1;
A23: born o in succ (born x) by SURREALO:1, A21, ORDINAL1:8;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A24: o in dom (S . (born o)) by A20, PARTFUN1:def 2;
then A25: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A22, SURREALR:5;
A26: born o in dom S by SURREALO:1, A21, ORDINAL1:8, A1;
A27: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A23;
A28: y = (union (rng S)) . o by A18, A24, A26, SURREALR:2, A27;
o in dom (union (rng (S | (born x)))) by SURREALR:5, A22, A24;
hence y in (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) by A18, A28, A25, FUNCT_1:def 6; :: thesis:

end;

A29: (union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) c= R_ (sqrt_0 x)

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A30: y in (union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) ; :: thesis:
consider o being object such that
A31: ( o in dom (union (rng (S | (born x)))) & o in R_ (NonNegativePart x) & (union (rng (S | (born x)))) . o = y ) by A30, FUNCT_1:def 6;
reconsider o = o as Surreal by A31, SURREAL0:def 16;
set b = born o;
A32: o in R_ x by Th2, A31;
A33: o in Day (born o) by SURREAL0:def 18;
A34: o in (L_ x) \/ (R_ x) by A32, XBOOLE_0:def 3;
then A35: born o in born x by SURREALO:1;
A36: born o in succ (born x) by A34, SURREALO:1, ORDINAL1:8;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A37: o in dom (S . (born o)) by A33, PARTFUN1:def 2;
A38: born o in dom S by A34, SURREALO:1, ORDINAL1:8, A1;
A39: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A36;
(S . (born o)) . o = (union (rng S)) . o by A37, A38, SURREALR:2;
then y = sqrt o by A39, A31, A37, A35, SURREALR:5;
hence y in R_ (sqrt_0 x) by Def9, A31; :: thesis:

end;

A40: R_ (sqrt_0 x) c= (union (rng (S | (born x)))) .: (R_ (NonNegativePart x))

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in R_ (sqrt_0 x) ; :: thesis:
then consider o being Surreal such that
A41: ( y = sqrt o & o in R_ (NonNegativePart x) ) by Def9;
set b = born o;
A42: o in R_ x by Th2, A41;
A43: o in Day (born o) by SURREAL0:def 18;
A44: o in (L_ x) \/ (R_ x) by A42, XBOOLE_0:def 3;
then A45: born o in born x by SURREALO:1;
A46: born o in succ (born x) by A44, ORDINAL1:8, SURREALO:1;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A47: o in dom (S . (born o)) by A43, PARTFUN1:def 2;
then A48: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A45, SURREALR:5;
A49: born o in dom S by A44, ORDINAL1:8, SURREALO:1, A1;
A50: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A46;
A51: y = (union (rng S)) . o by A41, A47, A49, SURREALR:2, A50;
o in dom (union (rng (S | (born x)))) by SURREALR:5, A45, A47;
hence y in (union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) by A41, A51, A48, FUNCT_1:def 6; :: thesis:

end;

A52: (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) = L_ (sqrt_0 x) by A6, A17, XBOOLE_0:def 10;
(union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) = R_ (sqrt_0 x) by A29, A40, XBOOLE_0:def 10;
hence sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by A5, A52; :: thesis: