let i be Integer; :: thesis: for p being Nat
for x being Surreal holds
( [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] implies x == uDyadic . ((i + 1) / (2 |^ p)) ) )
let p be Nat; :: thesis: for x being Surreal holds
( [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] implies x == uDyadic . ((i + 1) / (2 |^ p)) ) )
let x be Surreal; :: thesis: ( [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] implies x == uDyadic . ((i + 1) / (2 |^ p)) ) )
i + 0 < i + 2 by XREAL_1:6;
then i / (2 |^ p) < (i + 2) / (2 |^ p) by XREAL_1:74;
hence [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] is Surreal by SURREALO:22, Th24; :: thesis: ( x = [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] implies x == uDyadic . ((i + 1) / (2 |^ p)) )
assume A1: x = [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] ; :: thesis: x == uDyadic . ((i + 1) / (2 |^ p))

per cases ( p = 0 or p > 0 ) ;

suppose p = 0 ; :: thesis: x == uDyadic . ((i + 1) / (2 |^ p))

then A2: 2 |^ p = 1 by NEWTON:4;
set j = i + 1;
A3: ( (i + 1) - 1 = i & (i + 1) + 1 = i + 2 ) ;
( uDyadic . (i / (2 |^ p)) = uInt . i & uDyadic . ((i + 1) / (2 |^ p)) = uInt . (i + 1) & uDyadic . ((i + 2) / (2 |^ p)) = uInt . (i + 2) ) by A2, Def5;
hence x == uDyadic . ((i + 1) / (2 |^ p)) by A1, Th10, A3; :: thesis: verum

end;

suppose A4: p > 0 ; :: thesis: x == uDyadic . ((i + 1) / (2 |^ p))

per cases ( i + 1 > 0 or i + 1 = 0 or i + 1 < 0 ) ;

suppose i + 1 > 0 ; :: thesis: x == uDyadic . ((i + 1) / (2 |^ p))

then i is Element of NAT by INT_1:3, INT_1:7;
hence x == uDyadic . ((i + 1) / (2 |^ p)) by A1, A4, Lm7; :: thesis: verum

end;

suppose A5: i + 1 = 0 ; :: thesis: x == uDyadic . ((i + 1) / (2 |^ p))

A6: ( 0_No = uInt . 0 & uInt . 0 = uDyadic . 0 ) by Def1, Def5;
(- 1) / (2 |^ p) < 0 ;
then A7: ( L_ x << {0_No} & {x} << R_ 0_No ) by A1, A6, SURREALO:21, A5, Th24;
( L_ 0_No << {x} & {0_No} << R_ x ) by A5, A1, A6, SURREALO:21, Th24;
hence x == uDyadic . ((i + 1) / (2 |^ p)) by A6, A5, A7, SURREAL0:43; :: thesis: verum

end;

suppose i + 1 < 0 ; :: thesis: x == uDyadic . ((i + 1) / (2 |^ p))

then i + 1 <= - 1 by INT_1:8;
then (i + 1) + 1 <= (- 1) + 1 by XREAL_1:6;
then reconsider n = - (i + 2) as Element of NAT by INT_1:3;
(n + 2) / (2 |^ p) = - ((- (n + 2)) / (2 |^ p)) by XCMPLX_1:190;
then uDyadic . ((n + 2) / (2 |^ p)) = - (uDyadic . (i / (2 |^ p))) by Th27;
then A8: -- (L_ x) = {(uDyadic . ((n + 2) / (2 |^ p)))} by A1, SURREALR:21;
n / (2 |^ p) = - ((i + 2) / (2 |^ p)) by XCMPLX_1:187;
then uDyadic . (n / (2 |^ p)) = - (uDyadic . ((i + 2) / (2 |^ p))) by Th27;
then -- (R_ x) = {(uDyadic . (n / (2 |^ p)))} by A1, SURREALR:21;
then - x = [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] by A8, SURREALR:7;
then - x == uDyadic . ((n + 1) / (2 |^ p)) by A4, Lm7;
then ( x = - (- x) & - (- x) == - (uDyadic . ((n + 1) / (2 |^ p))) ) by SURREALR:10;
then A9: x == uDyadic . (- ((n + 1) / (2 |^ p))) by Th27;
- (n + 1) = i + 1 ;
hence x == uDyadic . ((i + 1) / (2 |^ p)) by A9, XCMPLX_1:187; :: thesis: verum

end;

end;

end;

end;