let x be Surreal; :: thesis: ( ( for y being Surreal st y in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
y == 0_No ) implies sqrt x = sqrt_0 x )
assume A1: for y being Surreal st y in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
y == 0_No ; :: thesis: sqrt x = sqrt_0 x
defpred S₁[ Nat] means ( (sqrtL ((sqrt_0 x),x)) . $1 = L_ (sqrt_0 x) & (sqrtR ((sqrt_0 x),x)) . $1 = R_ (sqrt_0 x) );
A2: S₁[ 0 ] by Th6;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set S0 = sqrt_0 x;
set n1 = n + 1;
(sqrtL ((sqrt_0 x),x)) . 0 c= (sqrtL ((sqrt_0 x),x)) . (n + 1) by Th7;
then A5: L_ (sqrt_0 x) c= (sqrtL ((sqrt_0 x),x)) . (n + 1) by Th6;
(sqrtL ((sqrt_0 x),x)) . (n + 1) c= L_ (sqrt_0 x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (sqrtL ((sqrt_0 x),x)) . (n + 1) or o in L_ (sqrt_0 x) )
assume A6: ( o in (sqrtL ((sqrt_0 x),x)) . (n + 1) & not o in L_ (sqrt_0 x) ) ; :: thesis: contradiction
o in ((sqrtL ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A6, Th8;
then o in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) by A4, A6, XBOOLE_0:def 3;
then consider x1, y1 being Surreal such that
A7: ( x1 in (sqrtL ((sqrt_0 x),x)) . n & y1 in (sqrtR ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & o = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
consider l being Surreal such that
A8: ( x1 = sqrt l & l in L_ (NonNegativePart x) ) by A4, A7, Def9;
l in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A8, XBOOLE_0:def 3;
then l == 0_No by A1;
then A9: x1 == 0_No by A8, Th19;
consider r being Surreal such that
A10: ( y1 = sqrt r & r in R_ (NonNegativePart x) ) by A4, A7, Def9;
r in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A10, XBOOLE_0:def 3;
then r == 0_No by A1;
then y1 == 0_No by A10, Th19;
then x1 + y1 == 0_No + 0_No by A9, SURREALR:66;
hence contradiction by A7; :: thesis: verum

end;

hence (sqrtL ((sqrt_0 x),x)) . (n + 1) = L_ (sqrt_0 x) by A5, XBOOLE_0:def 10; :: thesis: (sqrtR ((sqrt_0 x),x)) . (n + 1) = R_ (sqrt_0 x)
(sqrtR ((sqrt_0 x),x)) . 0 c= (sqrtR ((sqrt_0 x),x)) . (n + 1) by Th7;
then A11: R_ (sqrt_0 x) c= (sqrtR ((sqrt_0 x),x)) . (n + 1) by Th6;
(sqrtR ((sqrt_0 x),x)) . (n + 1) c= R_ (sqrt_0 x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (sqrtR ((sqrt_0 x),x)) . (n + 1) or o in R_ (sqrt_0 x) )
assume A12: ( o in (sqrtR ((sqrt_0 x),x)) . (n + 1) & not o in R_ (sqrt_0 x) ) ; :: thesis: contradiction
o 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 A12, Th8;
then ( o in ((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n))) or o in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

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

suppose o in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) ; :: thesis: contradiction

then consider x1, y1 being Surreal such that
A13: ( x1 in (sqrtL ((sqrt_0 x),x)) . n & y1 in (sqrtL ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & o = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
consider l being Surreal such that
A14: ( x1 = sqrt l & l in L_ (NonNegativePart x) ) by Def9, A4, A13;
l in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A14, XBOOLE_0:def 3;
then l == 0_No by A1;
then A15: x1 == 0_No by A14, Th19;
consider r being Surreal such that
A16: ( y1 = sqrt r & r in L_ (NonNegativePart x) ) by Def9, A4, A13;
r in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A16, XBOOLE_0:def 3;
then r == 0_No by A1;
then y1 == 0_No by A16, Th19;
then x1 + y1 == 0_No + 0_No by A15, SURREALR:66;
hence contradiction by A13; :: thesis: verum

end;

suppose o in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis: contradiction

then consider x1, y1 being Surreal such that
A17: ( x1 in (sqrtR ((sqrt_0 x),x)) . n & y1 in (sqrtR ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & o = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
consider l being Surreal such that
A18: ( x1 = sqrt l & l in R_ (NonNegativePart x) ) by Def9, A4, A17;
l in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A18, XBOOLE_0:def 3;
then l == 0_No by A1;
then A19: x1 == 0_No by A18, Th19;
consider r being Surreal such that
A20: ( y1 = sqrt r & r in R_ (NonNegativePart x) ) by Def9, A4, A17;
r in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A20, XBOOLE_0:def 3;
then r == 0_No by A1;
then y1 == 0_No by A20, Th19;
then x1 + y1 == 0_No + 0_No by A19, SURREALR:66;
hence contradiction by A17; :: thesis: verum

end;

end;

end;

hence (sqrtR ((sqrt_0 x),x)) . (n + 1) = R_ (sqrt_0 x) by A11, XBOOLE_0:def 10; :: thesis: verum

end;

A21: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
A22: sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by Th15;
A23: L_ (sqrt x) = L_ (sqrt_0 x)

proof

thus L_ (sqrt x) c= L_ (sqrt_0 x) :: according to XBOOLE_0:def 10 :: thesis: L_ (sqrt_0 x) c= L_ (sqrt x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in L_ (sqrt x) or o in L_ (sqrt_0 x) )
assume o in L_ (sqrt x) ; :: thesis: o in L_ (sqrt_0 x)
then consider n being object such that
A24: ( n in dom (sqrtL ((sqrt_0 x),x)) & o in (sqrtL ((sqrt_0 x),x)) . n ) by A22, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A24;
(sqrtL ((sqrt_0 x),x)) . n = L_ (sqrt_0 x) by A21;
hence o in L_ (sqrt_0 x) by A24; :: thesis: verum

end;

thus L_ (sqrt_0 x) c= L_ (sqrt x) by A2, A22, ABCMIZ_1:1; :: thesis: verum

end;

R_ (sqrt x) = R_ (sqrt_0 x)

proof

thus R_ (sqrt x) c= R_ (sqrt_0 x) :: according to XBOOLE_0:def 10 :: thesis: R_ (sqrt_0 x) c= R_ (sqrt x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in R_ (sqrt x) or o in R_ (sqrt_0 x) )
assume o in R_ (sqrt x) ; :: thesis: o in R_ (sqrt_0 x)
then consider n being object such that
A25: ( n in dom (sqrtR ((sqrt_0 x),x)) & o in (sqrtR ((sqrt_0 x),x)) . n ) by A22, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def5;
then reconsider n = n as Nat by A25;
(sqrtR ((sqrt_0 x),x)) . n = R_ (sqrt_0 x) by A21;
hence o in R_ (sqrt_0 x) by A25; :: thesis: verum

end;

thus R_ (sqrt_0 x) c= R_ (sqrt x) by A2, A22, ABCMIZ_1:1; :: thesis: verum

end;

hence sqrt x = sqrt_0 x by A23, XTUPLE_0:2; :: thesis: verum