let d be Dyadic; :: thesis: uDyadic . d in born_eq_set (uDyadic . d)
A1: - (- d) = d ;

per cases ( d is Integer or ( d < 0 & d is not Integer ) or ( 0 <= d & d is not Integer ) ) ;

suppose d is Integer ; :: thesis: uDyadic . d in born_eq_set (uDyadic . d)

then reconsider i = d as Integer ;
A2: uDyadic . d = uInt . i by Def5;
born (uInt . i) = born_eq (uInt . i) by SURREALO:48;
then uInt . i in Day (born_eq (uInt . i)) by SURREAL0:def 18;
hence uDyadic . d in born_eq_set (uDyadic . d) by A2, SURREALO:def 6; :: thesis: verum

end;

suppose A3: ( d < 0 & d is not Integer ) ; :: thesis: uDyadic . d in born_eq_set (uDyadic . d)

then ( 0 < - d & - d is not Integer ) by A1;
then consider n, m, p being Nat such that
A4: ( - d = n + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) ) by Th28;
set D = uDyadic . (- d);
A5: 0_No <= uDyadic . (- d) by A3, Th29;
A6: born (uDyadic . (- d)) = (n + (p + 1)) + 1 by A4, Th26;
A7: uDyadic . (- d) = - (uDyadic . d) by Th27;
then A8: born (uDyadic . (- d)) = born (uDyadic . d) by SURREALR:12;
for y being Surreal st y == uDyadic . (- d) holds
born (uDyadic . (- d)) c= born y

proof

let y be Surreal; :: thesis: ( y == uDyadic . (- d) implies born (uDyadic . (- d)) c= born y )
assume A9: ( y == uDyadic . (- d) & not born (uDyadic . (- d)) c= born y ) ; :: thesis: contradiction
A10: born y in Segm ((n + (p + 1)) + 1) by A6, A9, ORDINAL1:16;
reconsider By = born y as Nat by A6, A9;
By < (n + (p + 1)) + 1 by A10, NAT_1:44;
then By <= (n + p) + 1 by NAT_1:13;
then Segm By c= Segm ((n + p) + 1) by NAT_1:39;
then A11: ( y in Day By & Day By c= Day ((n + p) + 1) ) by SURREAL0:def 18, SURREAL0:35;
not y == uDyadic . ((n + p) + 1)

proof

assume y == uDyadic . ((n + p) + 1) ; :: thesis: contradiction
then ( - d <= (n + p) + 1 & (n + p) + 1 <= - d ) by Th24, A9, SURREALO:4;
then - d = n + (p + 1) by XXREAL_0:1;
hence contradiction by NAT_1:14, A4, XREAL_1:189; :: thesis: verum

end;

then consider x1, y1, p1 being Nat such that
A12: ( y == uDyadic . (x1 + (y1 / (2 |^ p1))) & y1 < 2 |^ p1 & x1 + p1 < (n + p) + 1 ) by A5, A9, SURREALO:4, A11, Th25;
( - d <= x1 + (y1 / (2 |^ p1)) & x1 + (y1 / (2 |^ p1)) <= - d ) by Th24, A9, A12, SURREALO:4;
then A13: n + (((2 * m) + 1) / (2 |^ (p + 1))) = x1 + (y1 / (2 |^ p1)) by A4, XXREAL_0:1;
( 0 <= ((2 * m) + 1) / (2 |^ (p + 1)) & ((2 * m) + 1) / (2 |^ (p + 1)) < 1 & 0 <= y1 / (2 |^ p1) & y1 / (2 |^ p1) < 1 ) by A4, A12, XREAL_1:191;
then ( n + 0 <= n + (((2 * m) + 1) / (2 |^ (p + 1))) & n + (((2 * m) + 1) / (2 |^ (p + 1))) < n + 1 & x1 + 0 <= x1 + (y1 / (2 |^ p1)) & x1 + (y1 / (2 |^ p1)) < x1 + 1 ) by XREAL_1:6;
then ( n < x1 + 1 & x1 < n + 1 ) by A13, XXREAL_0:2;
then ( n <= x1 & x1 <= n ) by NAT_1:13;
then A14: x1 = n by XXREAL_0:1;
x1 + p1 < n + (p + 1) by A12;
then p1 < p + 1 by A14, XREAL_1:6;
then p1 <= p by NAT_1:13;
then reconsider P = p - p1 as Nat by NAT_1:21;
p = p1 + P ;
then A15: ( 2 |^ p = (2 |^ p1) * (2 |^ P) & 2 |^ (p + 1) = 2 * (2 |^ p) ) by NEWTON:6, NEWTON:8;
((2 * m) + 1) * (2 |^ p1) = y1 * (2 |^ (p + 1)) by A13, A14, XCMPLX_1:95
.= ((y1 * (2 |^ P)) * 2) * (2 |^ p1) by A15 ;
hence contradiction by XCMPLX_1:5; :: thesis: verum

end;

then ( born_eq (uDyadic . d) = born_eq (uDyadic . (- d)) & born_eq (uDyadic . (- d)) = born (uDyadic . (- d)) ) by A7, SURREALO:def 5, SURREALR:13;
then uDyadic . d in Day (born_eq (uDyadic . d)) by A8, SURREAL0:def 18;
hence uDyadic . d in born_eq_set (uDyadic . d) by SURREALO:def 6; :: thesis: verum

end;

suppose A16: ( 0 <= d & d is not Integer ) ; :: thesis: uDyadic . d in born_eq_set (uDyadic . d)

then consider n, m, p being Nat such that
A17: ( d = n + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) ) by Th28;
set D = uDyadic . d;
A18: 0_No <= uDyadic . d by A16, Th29;
A19: born (uDyadic . d) = (n + (p + 1)) + 1 by A17, Th26;
for y being Surreal st y == uDyadic . d holds
born (uDyadic . d) c= born y

proof

let y be Surreal; :: thesis: ( y == uDyadic . d implies born (uDyadic . d) c= born y )
assume A20: ( y == uDyadic . d & not born (uDyadic . d) c= born y ) ; :: thesis: contradiction
A21: born y in Segm ((n + (p + 1)) + 1) by A19, A20, ORDINAL1:16;
reconsider By = born y as Nat by A19, A20;
By < (n + (p + 1)) + 1 by A21, NAT_1:44;
then By <= (n + p) + 1 by NAT_1:13;
then Segm By c= Segm ((n + p) + 1) by NAT_1:39;
then A22: ( y in Day By & Day By c= Day ((n + p) + 1) ) by SURREAL0:def 18, SURREAL0:35;
not y == uDyadic . ((n + p) + 1)

proof

assume y == uDyadic . ((n + p) + 1) ; :: thesis: contradiction
then ( d <= (n + p) + 1 & (n + p) + 1 <= d ) by Th24, A20, SURREALO:4;
then d = n + (p + 1) by XXREAL_0:1;
hence contradiction by NAT_1:14, A17, XREAL_1:189; :: thesis: verum

end;

then consider x1, y1, p1 being Nat such that
A23: ( y == uDyadic . (x1 + (y1 / (2 |^ p1))) & y1 < 2 |^ p1 & x1 + p1 < (n + p) + 1 ) by A18, A20, SURREALO:4, A22, Th25;
( d <= x1 + (y1 / (2 |^ p1)) & x1 + (y1 / (2 |^ p1)) <= d ) by Th24, A20, A23, SURREALO:4;
then A24: n + (((2 * m) + 1) / (2 |^ (p + 1))) = x1 + (y1 / (2 |^ p1)) by A17, XXREAL_0:1;
( 0 <= ((2 * m) + 1) / (2 |^ (p + 1)) & ((2 * m) + 1) / (2 |^ (p + 1)) < 1 & 0 <= y1 / (2 |^ p1) & y1 / (2 |^ p1) < 1 ) by A17, A23, XREAL_1:191;
then ( n + 0 <= n + (((2 * m) + 1) / (2 |^ (p + 1))) & n + (((2 * m) + 1) / (2 |^ (p + 1))) < n + 1 & x1 + 0 <= x1 + (y1 / (2 |^ p1)) & x1 + (y1 / (2 |^ p1)) < x1 + 1 ) by XREAL_1:6;
then ( n < x1 + 1 & x1 < n + 1 ) by A24, XXREAL_0:2;
then ( n <= x1 & x1 <= n ) by NAT_1:13;
then A25: x1 = n by XXREAL_0:1;
x1 + p1 < n + (p + 1) by A23;
then p1 < p + 1 by A25, XREAL_1:6;
then p1 <= p by NAT_1:13;
then reconsider P = p - p1 as Nat by NAT_1:21;
p = p1 + P ;
then A26: ( 2 |^ p = (2 |^ p1) * (2 |^ P) & 2 |^ (p + 1) = 2 * (2 |^ p) ) by NEWTON:6, NEWTON:8;
((2 * m) + 1) * (2 |^ p1) = y1 * (2 |^ (p + 1)) by A24, A25, XCMPLX_1:95
.= ((y1 * (2 |^ P)) * 2) * (2 |^ p1) by A26 ;
hence contradiction by XCMPLX_1:5; :: thesis: verum

end;

then born_eq (uDyadic . d) = born (uDyadic . d) by SURREALO:def 5;
then uDyadic . d in Day (born_eq (uDyadic . d)) by SURREAL0:def 18;
hence uDyadic . d in born_eq_set (uDyadic . d) by SURREALO:def 6; :: thesis: verum

end;

end;