let x, y be Surreal; :: thesis: ( 0_No <= x implies ( ( y = sqrt x implies ( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) & sqrt x is surreal ) )
defpred S₁[ Ordinal] means for x being Surreal st born x = $1 & 0_No <= x holds
( sqrt x is surreal & ( for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y ) ) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let x be Surreal; :: thesis: ( born x = D & 0_No <= x implies ( sqrt x is surreal & ( for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y ) ) ) )
assume A3: ( born x = D & 0_No <= x ) ; :: thesis: ( sqrt x is surreal & ( for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y ) ) )
set S = sqrt x;
set S0 = sqrt_0 x;
A4: sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by Th15;
defpred S₂[ Nat] means ( ( for y being Surreal st y in (sqrtL ((sqrt_0 x),x)) . $1 holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in (sqrtR ((sqrt_0 x),x)) . $1 holds
( 0_No < y & x < y * y ) ) );
set Nx = NonNegativePart x;
A5: S₂[ 0 ]

proof

thus for y being Surreal st y in (sqrtL ((sqrt_0 x),x)) . 0 holds
( 0_No <= y & y * y < x ) :: thesis: for y being Surreal st y in (sqrtR ((sqrt_0 x),x)) . 0 holds
( 0_No < y & x < y * y )

proof

let y be Surreal; :: thesis: ( y in (sqrtL ((sqrt_0 x),x)) . 0 implies ( 0_No <= y & y * y < x ) )
assume A6: y in (sqrtL ((sqrt_0 x),x)) . 0 ; :: thesis: ( 0_No <= y & y * y < x )
y in L_ (sqrt_0 x) by A6, Th6;
then consider l being Surreal such that
A7: ( y = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
A8: ( l in L_ x & 0_No <= l ) by Th2, A7;
A9: ( L_ x << {x} & x in {x} ) by SURREALO:11, TARSKI:def 1;
l in (L_ x) \/ (R_ x) by A8, XBOOLE_0:def 3;
then born l in D by A3, SURREALO:1;
then ( 0_No <= y & y * y == l ) by A2, A8, A7;
hence ( 0_No <= y & y * y < x ) by A9, A8, SURREALO:4; :: thesis: verum

end;

let y be Surreal; :: thesis: ( y in (sqrtR ((sqrt_0 x),x)) . 0 implies ( 0_No < y & x < y * y ) )
assume A10: y in (sqrtR ((sqrt_0 x),x)) . 0 ; :: thesis: ( 0_No < y & x < y * y )
y in R_ (sqrt_0 x) by A10, Th6;
then consider r being Surreal such that
A11: ( y = sqrt r & r in R_ (NonNegativePart x) ) by Def9;
A12: ( r in R_ x & 0_No <= r ) by A11, Th2;
then r in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then A13: born r in D by A3, SURREALO:1;
then A14: ( 0_No <= y & y * y == r ) by A2, A11, A12;
A15: ( x in {x} & {x} << R_ x ) by SURREALO:11, TARSKI:def 1;
then 0_No < r by A3, A12, SURREALO:4;
hence ( 0_No < y & x < y * y ) by A15, A12, A13, A2, A11, A14, SURREALO:4; :: thesis: verum

end;

A16: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A17: S₂[n] ; :: thesis: S₂[n + 1]
thus for y being Surreal st y in (sqrtL ((sqrt_0 x),x)) . (n + 1) holds
( 0_No <= y & y * y < x ) :: thesis: for y being Surreal st y in (sqrtR ((sqrt_0 x),x)) . (n + 1) holds
( 0_No < y & x < y * y )

proof

let y be Surreal; :: thesis: ( y in (sqrtL ((sqrt_0 x),x)) . (n + 1) implies ( 0_No <= y & y * y < x ) )
assume A18: y in (sqrtL ((sqrt_0 x),x)) . (n + 1) ; :: thesis: ( 0_No <= y & y * y < x )
y in ((sqrtL ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A18, Th8;

per cases then ( y in (sqrtL ((sqrt_0 x),x)) . n or y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

suppose y in (sqrtL ((sqrt_0 x),x)) . n ; :: thesis: ( 0_No <= y & y * y < x )

hence ( 0_No <= y & y * y < x ) by A17; :: thesis: verum

end;

suppose y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis: ( 0_No <= y & y * y < x )

then consider L1, R1 being Surreal such that
A19: ( L1 in (sqrtL ((sqrt_0 x),x)) . n & R1 in (sqrtR ((sqrt_0 x),x)) . n & not L1 + R1 == 0_No & y = (x +' (L1 * R1)) * ((L1 + R1) ") ) by Def2;
A20: ( 0_No <= L1 & 0_No <= R1 ) by A19, A17;
then 0_No + 0_No <= L1 + R1 by SURREALR:43;
then A21: 0_No <= (L1 + R1) " by A19, SURREALI:40;
0_No * R1 <= L1 * R1 by A20, SURREALR:75;
then 0_No + 0_No <= x + (L1 * R1) by A3, SURREALR:43;
then A22: 0_No * ((L1 + R1) ") <= (x +' (L1 * R1)) * ((L1 + R1) ") by A21, SURREALR:75;
( L1 * L1 < x & x < R1 * R1 ) by A19, A17;
then ( 0_No < x - (L1 * L1) & x - (R1 * R1) < 0_No ) by SURREALR:45, SURREALR:46;
then A23: (x - (L1 * L1)) * (x - (R1 * R1)) < 0_No by SURREALR:74;
((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) == (x - (L1 * L1)) * (x - (R1 * R1)) by Lm2;
then ((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) < 0_No by A23, SURREALO:4;
then A24: (x * x) + ((L1 * R1) * (L1 * R1)) < (x * (L1 * L1)) + (x * (R1 * R1)) by SURREALR:46;
A25: x * ((L1 + R1) * (L1 + R1)) == ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + (x * (R1 * L1))) by Lm1;
A26: (x + (L1 * R1)) * (x + (L1 * R1)) == ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by SURREALR:76;
((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) < ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by A24, SURREALR:44;
then ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + (x * (L1 * R1))) < x * ((L1 + R1) * (L1 + R1)) by A25, SURREALO:4;
then (x + (L1 * R1)) * (x + (L1 * R1)) < x * ((L1 + R1) * (L1 + R1)) by A26, SURREALO:4;
hence ( 0_No <= y & y * y < x ) by A22, A19, Th17; :: thesis: verum

end;

end;

end;

let y be Surreal; :: thesis: ( y in (sqrtR ((sqrt_0 x),x)) . (n + 1) implies ( 0_No < y & x < y * y ) )
assume A27: y in (sqrtR ((sqrt_0 x),x)) . (n + 1) ; :: thesis: ( 0_No < y & x < y * y )
y in (((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A27, Th8;
then ( y in ((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n))) or y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

per cases then ( y in (sqrtR ((sqrt_0 x),x)) . n or y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) or y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

suppose y in (sqrtR ((sqrt_0 x),x)) . n ; :: thesis: ( 0_No < y & x < y * y )

hence ( 0_No < y & x < y * y ) by A17; :: thesis: verum

end;

suppose y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) ; :: thesis: ( 0_No < y & x < y * y )

then consider L1, R1 being Surreal such that
A28: ( L1 in (sqrtL ((sqrt_0 x),x)) . n & R1 in (sqrtL ((sqrt_0 x),x)) . n & not L1 + R1 == 0_No & y = (x +' (L1 * R1)) * ((L1 + R1) ") ) by Def2;
A29: ( 0_No <= L1 & 0_No <= R1 ) by A28, A17;
then 0_No + 0_No <= L1 + R1 by SURREALR:43;
then A30: 0_No < (L1 + R1) " by A28, SURREALI:40;
A31: (sqrtL ((sqrt_0 x),x)) . n c= Union (sqrtL ((sqrt_0 x),x)) by ABCMIZ_1:1;
0_No * R1 <= L1 * R1 by A29, SURREALR:75;
then A32: 0_No + 0_No < x + (L1 * R1) by A31, Th18, A28, SURREALR:44;
( 0_No < x - (L1 * L1) & 0_No < x - (R1 * R1) ) by A28, A17, SURREALR:45;
then A33: 0_No < (x - (L1 * L1)) * (x - (R1 * R1)) by SURREALR:72;
((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) == (x - (L1 * L1)) * (x - (R1 * R1)) by Lm2;
then 0_No < ((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) by A33, SURREALO:4;
then A34: (x * (L1 * L1)) + (x * (R1 * R1)) < (x * x) + ((L1 * R1) * (L1 * R1)) by SURREALR:45;
A35: x * ((L1 + R1) * (L1 + R1)) == ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + (x * (R1 * L1))) by Lm1;
A36: (x + (L1 * R1)) * (x + (L1 * R1)) == ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by SURREALR:76;
((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by A34, SURREALR:44;
then x * ((L1 + R1) * (L1 + R1)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + (x * (L1 * R1))) by A35, SURREALO:4;
then x * ((L1 + R1) * (L1 + R1)) < (x + (L1 * R1)) * (x + (L1 * R1)) by A36, SURREALO:4;
hence ( 0_No < y & x < y * y ) by A32, A28, Th17, A30, SURREALR:72; :: thesis: verum

end;

suppose y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis: ( 0_No < y & x < y * y )

then consider L1, R1 being Surreal such that
A37: ( L1 in (sqrtR ((sqrt_0 x),x)) . n & R1 in (sqrtR ((sqrt_0 x),x)) . n & not L1 + R1 == 0_No & y = (x +' (L1 * R1)) * ((L1 + R1) ") ) by Def2;
A38: ( 0_No < L1 & 0_No < R1 ) by A37, A17;
( 0_No < L1 & 0_No <= R1 ) by A37, A17;
then 0_No + 0_No < L1 + R1 by SURREALR:44;
then A39: 0_No < (L1 + R1) " by A37, SURREALI:40;
0_No < L1 * R1 by A38, SURREALR:72;
then A40: 0_No + 0_No < x + (L1 * R1) by A3, SURREALR:44;
( x < L1 * L1 & x < R1 * R1 ) by A37, A17;
then ( x - (L1 * L1) < 0_No & x - (R1 * R1) < 0_No ) by SURREALR:46;
then A41: 0_No < (x - (L1 * L1)) * (x - (R1 * R1)) by SURREALR:72;
((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) == (x - (L1 * L1)) * (x - (R1 * R1)) by Lm2;
then 0_No < ((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) by A41, SURREALO:4;
then A42: (x * (L1 * L1)) + (x * (R1 * R1)) < (x * x) + ((L1 * R1) * (L1 * R1)) by SURREALR:45;
A43: x * ((L1 + R1) * (L1 + R1)) == ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + (x * (R1 * L1))) by Lm1;
A44: (x + (L1 * R1)) * (x + (L1 * R1)) == ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by SURREALR:76;
((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by A42, SURREALR:44;
then x * ((L1 + R1) * (L1 + R1)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + (x * (L1 * R1))) by A43, SURREALO:4;
then x * ((L1 + R1) * (L1 + R1)) < (x + (L1 * R1)) * (x + (L1 * R1)) by A44, SURREALO:4;
hence ( 0_No < y & x < y * y ) by A40, A37, A39, SURREALR:72, Th17; :: thesis: verum

end;

end;

end;

A45: for n being Nat holds S₂[n] from NAT_1:sch 2(A5, A16);
A46: for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x )

proof

let y be Surreal; :: thesis: ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) )
assume y in L_ (sqrt x) ; :: thesis: ( 0_No <= y & y * y < x )
then consider n being object such that
A47: ( n in dom (sqrtL ((sqrt_0 x),x)) & y in (sqrtL ((sqrt_0 x),x)) . n ) by A4, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A47;
S₂[n] by A45;
hence ( 0_No <= y & y * y < x ) by A47; :: thesis: verum

end;

A48: for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y )

proof

let y be Surreal; :: thesis: ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) )
assume y in R_ (sqrt x) ; :: thesis: ( 0_No < y & x < y * y )
then consider n being object such that
A49: ( n in dom (sqrtR ((sqrt_0 x),x)) & y in (sqrtR ((sqrt_0 x),x)) . n ) by A4, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def5;
then reconsider n = n as Nat by A49;
S₂[n] by A45;
hence ( 0_No < y & x < y * y ) by A49; :: thesis: verum

end;

A50: L_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in L_ (sqrt_0 x) or o is surreal )
assume o in L_ (sqrt_0 x) ; :: thesis: o is surreal
then consider l being Surreal such that
A51: ( o = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
A52: ( l in L_ x & 0_No <= l ) by Th2, A51;
then l in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then born l in D by A3, SURREALO:1;
hence o is surreal by A51, A52, A2; :: thesis: verum

end;

R_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in R_ (sqrt_0 x) or o is surreal )
assume o in R_ (sqrt_0 x) ; :: thesis: o is surreal
then consider r being Surreal such that
A53: ( o = sqrt r & r in R_ (NonNegativePart x) ) by Def9;
A54: ( r in R_ x & 0_No <= r ) by Th2, A53;
then r in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then born r in D by A3, SURREALO:1;
hence o is surreal by A53, A54, A2; :: thesis: verum

end;

then ( Union (sqrtL ((sqrt_0 x),x)) is surreal-membered & Union (sqrtR ((sqrt_0 x),x)) is surreal-membered ) by A50, Th10;
then consider M being Ordinal such that
A55: for o being object st o in (Union (sqrtL ((sqrt_0 x),x))) \/ (Union (sqrtR ((sqrt_0 x),x))) holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
Union (sqrtL ((sqrt_0 x),x)) << Union (sqrtR ((sqrt_0 x),x))

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in Union (sqrtL ((sqrt_0 x),x)) or not r in Union (sqrtR ((sqrt_0 x),x)) or not r <= l )
assume A56: ( l in Union (sqrtL ((sqrt_0 x),x)) & r in Union (sqrtR ((sqrt_0 x),x)) & r <= l ) ; :: thesis: contradiction
consider n being object such that
A57: ( n in dom (sqrtL ((sqrt_0 x),x)) & l in (sqrtL ((sqrt_0 x),x)) . n ) by A56, CARD_5:2;
consider k being object such that
A58: ( k in dom (sqrtR ((sqrt_0 x),x)) & r in (sqrtR ((sqrt_0 x),x)) . k ) by A56, CARD_5:2;
( dom (sqrtL ((sqrt_0 x),x)) = NAT & NAT = dom (sqrtR ((sqrt_0 x),x)) ) by Def4, Def5;
then reconsider n = n, k = k as Nat by A57, A58;
A59: ( S₂[n] & S₂[k] ) by A45;
then A60: ( 0_No <= l & l * l < x & 0_No <= r & x < r * r ) by A57, A58;
then ( r * r <= r * l & r * l <= l * l ) by A56, SURREALR:75;
then r * r <= l * l by SURREALO:4;
then x <= l * l by A60, SURREALO:4;
hence contradiction by A57, A59; :: thesis: verum

end;

then [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] in Day M by A55, SURREAL0:46;
then reconsider S = sqrt x as Surreal by Th15;
A61: for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x )

proof

let y be Surreal; :: thesis: ( y = sqrt x implies ( 0_No <= y & y * y == x ) )
assume A62: y = sqrt x ; :: thesis: ( 0_No <= y & y * y == x )
A63: L_ 0_No << {y} ;
{0_No} << R_ y

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {0_No} or not r in R_ y or not r <= l )
assume A64: ( l in {0_No} & r in R_ y ) ; :: thesis: not r <= l
consider n being object such that
A65: ( n in dom (sqrtR ((sqrt_0 x),x)) & r in (sqrtR ((sqrt_0 x),x)) . n ) by CARD_5:2, A4, A62, A64;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def5;
then reconsider n = n as Nat by A65;
r in (sqrtR ((sqrt_0 x),x)) . n by A65;
then 0_No < r by A45;
hence not r <= l by A64, TARSKI:def 1; :: thesis: verum

end;

hence A66: 0_No <= y by A63, SURREAL0:43; :: thesis: y * y == x
A67: y * y = [((comp ((L_ y),y,y,(L_ y))) \/ (comp ((R_ y),y,y,(R_ y)))),((comp ((L_ y),y,y,(R_ y))) \/ (comp ((R_ y),y,y,(L_ y))))] by SURREALR:50;
A68: L_ (y * y) << {x}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ (y * y) or not b in {x} or not b <= a )
assume A69: ( a in L_ (y * y) & b in {x} ) ; :: thesis: not b <= a

per cases ( a in comp ((L_ y),y,y,(L_ y)) or a in comp ((R_ y),y,y,(R_ y)) ) by XBOOLE_0:def 3, A67, A69;

suppose a in comp ((L_ y),y,y,(L_ y)) ; :: thesis: not b <= a

then consider x1, y1 being Surreal such that
A70: ( a = ((x1 * y) + (y * y1)) - (x1 * y1) & x1 in L_ y & y1 in L_ y ) by SURREALR:def 15;
consider n being object such that
A71: ( n in dom (sqrtL ((sqrt_0 x),x)) & x1 in (sqrtL ((sqrt_0 x),x)) . n ) by A70, A4, A62, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A71;
consider m being object such that
A72: ( m in dom (sqrtL ((sqrt_0 x),x)) & y1 in (sqrtL ((sqrt_0 x),x)) . m ) by A70, A4, A62, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n, m = m as Nat by A72;
set nm = n + m;
A73: ( n <= n + m & m <= n + m ) by NAT_1:11;
then A74: ( (sqrtL ((sqrt_0 x),x)) . n c= (sqrtL ((sqrt_0 x),x)) . (n + m) & (sqrtL ((sqrt_0 x),x)) . m c= (sqrtL ((sqrt_0 x),x)) . (n + m) ) by Th7;
A75: (sqrtL ((sqrt_0 x),x)) . n c= Union (sqrtL ((sqrt_0 x),x)) by ABCMIZ_1:1;
set X = x + (x1 * y1);
A76: ( 0_No <= x1 & 0_No <= y1 ) by A73, A71, A72, A45;

per cases ( ( x1 == 0_No & y1 == 0_No ) or not x1 == 0_No or not y1 == 0_No ) ;

suppose ( x1 == 0_No & y1 == 0_No ) ; :: thesis: not b <= a

then ( x1 * y == 0_No * y & y * y1 == y * 0_No & x1 * y1 == 0_No * x1 ) by SURREALR:54;
then ( (x1 * y) + (y * y1) == 0_No + 0_No & - (x1 * y1) == - 0_No ) by SURREALR:65, SURREALR:66;
then a == 0_No + 0_No by A70, SURREALR:66;
then a < x by A75, A71, Th18, SURREALO:4;
hence not b <= a by A69, TARSKI:def 1; :: thesis: verum

end;

suppose A77: ( not x1 == 0_No or not y1 == 0_No ) ; :: thesis: not b <= a

then 0_No + 0_No < x1 + y1 by A76, SURREALR:44;
then A78: not x1 + y1 == 0_No ;
then (x + (x1 * y1)) * ((x1 + y1) ") in sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m))) by A74, A71, A72, Def2;
then (x + (x1 * y1)) * ((x1 + y1) ") in ((sqrtR ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then (x + (x1 * y1)) * ((x1 + y1) ") in (((sqrtR ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m))))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then A79: ( (x + (x1 * y1)) * ((x1 + y1) ") in (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) & (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) c= Union (sqrtR ((sqrt_0 x),x)) ) by Th8, ABCMIZ_1:1;
A80: ( y in {y} & {y} << R_ y ) by TARSKI:def 1, SURREALO:11;
then A81: y < (x + (x1 * y1)) * ((x1 + y1) ") by A79, A62, A4;
A82: y <= (x + (x1 * y1)) * ((x1 + y1) ") by A80, A79, A62, A4;
A83: (x1 + y1) * ((x1 + y1) ") == 1_No by A78, SURREALI:33;
A84: (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) ")))

proof

per cases ( 0_No < x1 or 0_No < y1 ) by A73, A71, A72, A45, A77;

suppose 0_No < x1 ; :: thesis: (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) ")))

then ( x1 * y < x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) & y1 * y <= y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) ) by A76, A81, A82, SURREALR:70, SURREALR:75;
hence (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) by SURREALR:44; :: thesis: verum

end;

suppose 0_No < y1 ; :: thesis: (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) ")))

then ( x1 * y <= x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) & y1 * y < y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) ) by A76, A81, A82, SURREALR:70, SURREALR:75;
hence (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) by SURREALR:44; :: thesis: verum

end;

end;

end;

( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) & (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) ) by SURREALR:67, SURREALR:69;
then ( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) & ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) == 1_No * (x + (x1 * y1)) ) by A83, SURREALR:54, SURREALO:4;
then (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == 1_No * (x + (x1 * y1)) by SURREALO:4;
then (x1 * y) + (y * y1) < x + (x1 * y1) by A84, SURREALO:4;
then A85: ((x1 * y) + (y * y1)) + (- (x1 * y1)) < (x + (x1 * y1)) + (- (x1 * y1)) by SURREALR:44;
(x1 * y1) - (x1 * y1) == 0_No by SURREALR:39;
then ( (x + (x1 * y1)) + (- (x1 * y1)) = x + ((x1 * y1) + (- (x1 * y1))) & x + ((x1 * y1) + (- (x1 * y1))) == x + 0_No ) by SURREALR:37, SURREALR:66;
then a < x by A70, A85, SURREALO:4;
hence not b <= a by A69, TARSKI:def 1; :: thesis: verum

end;

end;

end;

suppose a in comp ((R_ y),y,y,(R_ y)) ; :: thesis: not b <= a

then consider x1, y1 being Surreal such that
A86: ( a = ((x1 * y) + (y * y1)) - (x1 * y1) & x1 in R_ y & y1 in R_ y ) by SURREALR:def 15;
consider n being object such that
A87: ( n in dom (sqrtR ((sqrt_0 x),x)) & x1 in (sqrtR ((sqrt_0 x),x)) . n ) by A86, A4, A62, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def5;
then reconsider n = n as Nat by A87;
consider m being object such that
A88: ( m in dom (sqrtR ((sqrt_0 x),x)) & y1 in (sqrtR ((sqrt_0 x),x)) . m ) by A86, A4, A62, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def5;
then reconsider n = n, m = m as Nat by A88;
set nm = n + m;
A89: ( n <= n + m & m <= n + m ) by NAT_1:11;
then A90: ( (sqrtR ((sqrt_0 x),x)) . n c= (sqrtR ((sqrt_0 x),x)) . (n + m) & (sqrtR ((sqrt_0 x),x)) . m c= (sqrtR ((sqrt_0 x),x)) . (n + m) ) by Th7;
set X = x + (x1 * y1);
A91: ( 0_No < x1 & 0_No <= y1 ) by A89, A87, A88, A45;
then 0_No + 0_No < x1 + y1 by SURREALR:44;
then A92: not x1 + y1 == 0_No ;
then (x + (x1 * y1)) * ((x1 + y1) ") in sqrt (x,((sqrtR ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m))) by A87, A88, A90, Def2;
then (x + (x1 * y1)) * ((x1 + y1) ") in (((sqrtR ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m))))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then A93: ( (x + (x1 * y1)) * ((x1 + y1) ") in (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) & (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) c= Union (sqrtR ((sqrt_0 x),x)) ) by Th8, ABCMIZ_1:1;
A94: ( y in {y} & {y} << R_ y ) by TARSKI:def 1, SURREALO:11;
then A95: y < (x + (x1 * y1)) * ((x1 + y1) ") by A93, A62, A4;
A96: y <= (x + (x1 * y1)) * ((x1 + y1) ") by A93, A94, A62, A4;
A97: (x1 + y1) * ((x1 + y1) ") == 1_No by A92, SURREALI:33;
( x1 * y < x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) & y1 * y <= y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) ) by A91, A95, A96, SURREALR:70, SURREALR:75;
then A98: (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) by SURREALR:44;
( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) & (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) ) by SURREALR:67, SURREALR:69;
then ( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) & ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) == 1_No * (x + (x1 * y1)) ) by A97, SURREALR:54, SURREALO:4;
then (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == 1_No * (x + (x1 * y1)) by SURREALO:4;
then (x1 * y) + (y * y1) < x + (x1 * y1) by A98, SURREALO:4;
then A99: ((x1 * y) + (y * y1)) + (- (x1 * y1)) < (x + (x1 * y1)) + (- (x1 * y1)) by SURREALR:44;
(x1 * y1) - (x1 * y1) == 0_No by SURREALR:39;
then ( (x + (x1 * y1)) + (- (x1 * y1)) = x + ((x1 * y1) + (- (x1 * y1))) & x + ((x1 * y1) + (- (x1 * y1))) == x + 0_No ) by SURREALR:37, SURREALR:66;
then a < x by A86, A99, SURREALO:4;
hence not b <= a by A69, TARSKI:def 1; :: thesis: verum

end;

end;

end;

A100: {(y * y)} << R_ x

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in {(y * y)} or not b in R_ x or not b <= a )
assume A101: ( a in {(y * y)} & b in R_ x ) ; :: thesis: not b <= a
A102: ( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
then A103: 0_No < b by A101, A3, SURREALO:4;
A104: 0_No <= b by A102, A101, A3, SURREALO:4;
b in (L_ x) \/ (R_ x) by A101, XBOOLE_0:def 3;
then A105: born b in born x by SURREALO:1;
then reconsider sb = sqrt b as Surreal by A104, A2, A3;
A106: ( 0_No < sb & sb * sb == b ) by A103, A104, A105, A2, A3;
b in R_ (NonNegativePart x) by A101, A104, Def1;
then A107: ( sb in R_ (sqrt_0 x) & R_ (sqrt_0 x) = (sqrtR ((sqrt_0 x),x)) . 0 & (sqrtR ((sqrt_0 x),x)) . 0 c= Union (sqrtR ((sqrt_0 x),x)) ) by Th6, Def9, ABCMIZ_1:1;
( y in {y} & {y} << R_ y ) by TARSKI:def 1, SURREALO:11;
then ( y < sb & y <= sb ) by A107, A62, A4;
then ( y * y <= sb * y & sb * y < sb * sb ) by A106, A66, SURREALR:75, SURREALR:70;
then y * y < sb * sb by SURREALO:4;
then y * y < b by A106, SURREALO:4;
hence not b <= a by A101, TARSKI:def 1; :: thesis: verum

end;

A108: L_ x << {(y * y)}

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not b in L_ x or not a in {(y * y)} or not a <= b )
assume A109: ( b in L_ x & a in {(y * y)} ) ; :: thesis: not a <= b

per cases ( b < 0_No or 0_No <= b ) ;

suppose A110: b < 0_No ; :: thesis: not a <= b

0_No * y <= y * y by A66, SURREALR:75;
then b < y * y by A110, SURREALO:4;
hence not a <= b by A109, TARSKI:def 1; :: thesis: verum

end;

suppose A111: 0_No <= b ; :: thesis: not a <= b

b in (L_ x) \/ (R_ x) by A109, XBOOLE_0:def 3;
then A112: born b in born x by SURREALO:1;
then reconsider sb = sqrt b as Surreal by A111, A2, A3;
b in L_ (NonNegativePart x) by A109, A111, Def1;
then A113: ( sb in L_ (sqrt_0 x) & L_ (sqrt_0 x) = (sqrtL ((sqrt_0 x),x)) . 0 & (sqrtL ((sqrt_0 x),x)) . 0 c= Union (sqrtL ((sqrt_0 x),x)) ) by Th6, Def9, ABCMIZ_1:1;
A114: ( 0_No <= sb & sb * sb == b ) by A111, A112, A2, A3;
A115: ( y in {y} & L_ y << {y} ) by TARSKI:def 1, SURREALO:11;
then A116: ( sb < y & sb <= y ) by A113, A62, A4;
0_No < y by A114, A113, A62, A4, A115, SURREALO:4;
then ( sb * sb <= sb * y & sb * y < y * y ) by A116, A114, SURREALR:75, SURREALR:70;
then sb * sb < y * y by SURREALO:4;
then b < y * y by A114, SURREALO:4;
hence not a <= b by A109, TARSKI:def 1; :: thesis: verum

end;

end;

end;

{x} << R_ (y * y)

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not b in {x} or not a in R_ (y * y) or not a <= b )
assume A117: ( b in {x} & a in R_ (y * y) ) ; :: thesis: not a <= b
comp ((L_ y),y,y,(R_ y)) = comp ((R_ y),y,y,(L_ y)) by SURREALR:53;
then consider x1, y1 being Surreal such that
A118: ( a = ((x1 * y) + (y * y1)) - (x1 * y1) & x1 in L_ y & y1 in R_ y ) by A67, A117, SURREALR:def 15;
consider n being object such that
A119: ( n in dom (sqrtL ((sqrt_0 x),x)) & x1 in (sqrtL ((sqrt_0 x),x)) . n ) by A118, A4, A62, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A119;
consider m being object such that
A120: ( m in dom (sqrtR ((sqrt_0 x),x)) & y1 in (sqrtR ((sqrt_0 x),x)) . m ) by A118, A4, A62, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def5;
then reconsider n = n, m = m as Nat by A120;
set nm = n + m;
A121: ( n <= n + m & m <= n + m ) by NAT_1:11;
then A122: ( (sqrtL ((sqrt_0 x),x)) . n c= (sqrtL ((sqrt_0 x),x)) . (n + m) & (sqrtR ((sqrt_0 x),x)) . m c= (sqrtR ((sqrt_0 x),x)) . (n + m) ) by Th7;
set X = x + (x1 * y1);
A123: ( 0_No <= x1 & 0_No < y1 ) by A121, A119, A120, A45;
then 0_No + 0_No < x1 + y1 by SURREALR:44;
then A124: not x1 + y1 == 0_No ;
then (x + (x1 * y1)) * ((x1 + y1) ") in sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m))) by A122, A119, A120, Def2;
then (x + (x1 * y1)) * ((x1 + y1) ") in ((sqrtL ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then A125: ( (x + (x1 * y1)) * ((x1 + y1) ") in (sqrtL ((sqrt_0 x),x)) . ((n + m) + 1) & (sqrtL ((sqrt_0 x),x)) . ((n + m) + 1) c= Union (sqrtL ((sqrt_0 x),x)) ) by Th8, ABCMIZ_1:1;
A126: ( y in {y} & L_ y << {y} ) by TARSKI:def 1, SURREALO:11;
then A127: (x + (x1 * y1)) * ((x1 + y1) ") < y by A125, A62, A4;
A128: (x + (x1 * y1)) * ((x1 + y1) ") <= y by A126, A125, A62, A4;
A129: (x1 + y1) * ((x1 + y1) ") == 1_No by A124, SURREALI:33;
( x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) <= x1 * y & y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) < y1 * y ) by A123, A127, A128, SURREALR:70, SURREALR:75;
then A130: (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) < (x1 * y) + (y * y1) by SURREALR:44;
( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) & (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) ) by SURREALR:67, SURREALR:69;
then ( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) & ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) == 1_No * (x + (x1 * y1)) ) by A129, SURREALR:54, SURREALO:4;
then (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == 1_No * (x + (x1 * y1)) by SURREALO:4;
then x + (x1 * y1) < (x1 * y) + (y * y1) by A130, SURREALO:4;
then A131: (x + (x1 * y1)) + (- (x1 * y1)) < ((x1 * y) + (y * y1)) + (- (x1 * y1)) by SURREALR:44;
(x1 * y1) - (x1 * y1) == 0_No by SURREALR:39;
then ( (x + (x1 * y1)) + (- (x1 * y1)) = x + ((x1 * y1) + (- (x1 * y1))) & x + ((x1 * y1) + (- (x1 * y1))) == x + 0_No ) by SURREALR:37, SURREALR:66;
then x < a by A118, A131, SURREALO:4;
hence not a <= b by A117, TARSKI:def 1; :: thesis: verum

end;

hence y * y == x by A68, A100, SURREAL0:43, A108; :: thesis: verum

end;

A132: for y being Surreal st y = sqrt x holds
( ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) )

proof

let y be Surreal; :: thesis: ( y = sqrt x implies ( ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) )
assume A133: y = sqrt x ; :: thesis: ( ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) )
thus ( x == 0_No implies y == 0_No ) :: thesis: ( 0_No < x implies 0_No < y )

proof

assume A134: x == 0_No ; :: thesis: y == 0_No
0_No <= y by A133, A61;
then A135: ( L_ y << {0_No} & {0_No} << R_ y ) by A134, A133, A4, Th18, SURREAL0:43;
for z being Surreal st L_ y << {z} & {z} << R_ y holds
born 0_No c= born z

proof

let z be Surreal; :: thesis: ( L_ y << {z} & {z} << R_ y implies born 0_No c= born z )
assume ( L_ y << {z} & {z} << R_ y ) ; :: thesis: born 0_No c= born z
born 0_No = {} by SURREAL0:37;
hence born 0_No c= born z ; :: thesis: verum

end;

hence y == 0_No by SURREALO:16, A135; :: thesis: verum

end;

assume A136: ( 0_No < x & y <= 0_No ) ; :: thesis: contradiction
then A137: ( y == 0_No & y * y == x ) by A133, A61;
then y * 0_No == y * y by SURREALR:54;
hence contradiction by A136, A137, SURREALO:4; :: thesis: verum

end;

S is Surreal ;
hence ( sqrt x is surreal & ( for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y ) ) ) by A46, A48, A61, A132; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence ( 0_No <= x implies ( ( y = sqrt x implies ( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) & sqrt x is surreal ) ) ; :: thesis: verum