SURREALI

reconsider xx = x, yy = y as Surreal by A1;
let a1, a2 be Surreal; :: thesis:
assume that
A2: for x1, y1 being Surreal st x1 = x & y1 = y holds
a1 = x1 * y1 and
A3: for x1, y1 being Surreal st x1 = x & y1 = y holds
a2 = x1 * y1 ; :: thesis:
a1 = xx * yy by A2;
hence a1 = a2 by A3; :: thesis:

end;

:: deftheorem Def1 defines *' SURREALI:def 1 :

definition

let lamb, x be object ;
let X be set ;
let Inv be Function;

func divs (lamb,x,X,Inv) -> set means :Def2: :: SURREALI:def 2
for o being object holds
( o in it iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) );

defpred S₁[ object , object ] means $2 = (1_No +' (($1 +' (-' x)) *' lamb)) *' (Inv . $1);
A1: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z ;
consider D being set such that
A2: for x being object holds
( x in D iff ex y being object st
( y in X \ {0_No} & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take D ; :: thesis:
let o be object ; :: thesis:
thus ( o in D implies ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) :: thesis:

assume o in D ; :: thesis:
then consider y being object such that
A3: ( y in X \ {0_No} & S₁[y,o] ) by A2;
( y in X & y <> 0_No ) by A3, ZFMISC_1:56;
hence ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) by A3; :: thesis:

end;

given xL being object such that A4: ( xL in X & xL <> 0_No ) and
A5: o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ; :: thesis:
xL in X \ {0_No} by A4, ZFMISC_1:56;
hence o in D by A2, A5; :: thesis:

end;

let D1, D2 be set ; :: thesis:
assume that
A6: for o being object holds
( o in D1 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) and
A7: for o being object holds
( o in D2 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
( o in D1 iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) by A6;
hence ( o in D1 iff o in D2 ) by A7; :: thesis:

end;

hence D1 = D2 by TARSKI:2; :: thesis:

end;

:: deftheorem Def2 defines divs SURREALI:def 2 :

definition

let Lamb be set ;
let x be object ;
let X be set ;
let Inv be Function;

func divset (Lamb,x,X,Inv) -> set means :Def3: :: SURREALI:def 3
for o being object holds
( o in it iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) );

set D = { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb } ;
take U = union { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb } ; :: thesis:
let o be object ; :: thesis:
thus ( o in U implies ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) :: thesis:

assume o in U ; :: thesis:
then consider d being set such that
A1: ( o in d & d in { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb } ) by TARSKI:def 4;
ex l being Element of Lamb st
( d = divs (l,x,X,Inv) & l in Lamb ) by A1;
hence ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) by A1; :: thesis:

end;

given lamb being object such that A2: ( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ; :: thesis:
divs (lamb,x,X,Inv) in { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb } by A2;
hence o in U by A2, TARSKI:def 4; :: thesis:

end;

let D1, D2 be set ; :: thesis:
assume that
A3: for o being object holds
( o in D1 iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) and
A4: for o being object holds
( o in D2 iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
( o in D1 iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) by A3;
hence ( o in D1 iff o in D2 ) by A4; :: thesis:

end;

hence D1 = D2 by TARSKI:2; :: thesis:

end;

:: deftheorem Def3 defines divset SURREALI:def 3 :

definition

let x be object ;
let Inv be Function;

func transitions_of (x,Inv) -> Function means :Def4: :: SURREALI:def 4
( dom it = NAT & it . 0 = 1_No & ( for k being Nat holds
( it . k is pair & (it . (k + 1)) `1 = ((L_ (it . k)) \/ (divset ((L_ (it . k)),x,(R_ x),Inv))) \/ (divset ((R_ (it . k)),x,(L_ x),Inv)) & (it . (k + 1)) `2 = ((R_ (it . k)) \/ (divset ((L_ (it . k)),x,(L_ x),Inv))) \/ (divset ((R_ (it . k)),x,(R_ x),Inv)) ) ) );

deffunc H₁( object , object ) -> object = [(((L_ $2) \/ (divset ((L_ $2),x,(R_ x),Inv))) \/ (divset ((R_ $2),x,(L_ x),Inv))),(((R_ $2) \/ (divset ((L_ $2),x,(L_ x),Inv))) \/ (divset ((R_ $2),x,(R_ x),Inv)))];
consider f being Function such that
A1: ( dom f = NAT & f . 0 = 1_No & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 11();
take f ; :: thesis:
thus ( dom f = omega & f . 0 = 1_No ) by A1; :: thesis:
let k be Nat; :: thesis:
thus f . k is pair :: thesis:

suppose k = 0 ; :: thesis:

hence f . k is pair by A1; :: thesis:

end;

suppose k > 0 ; :: thesis:

then reconsider k1 = k - 1 as Nat by NAT_1:20;
f . (k1 + 1) = H₁(k1,f . k1) by A1;
hence f . k is pair ; :: thesis:

end;

f . (k + 1) = H₁(k,f . k) by A1;
hence ( (f . (k + 1)) `1 = ((L_ (f . k)) \/ (divset ((L_ (f . k)),x,(R_ x),Inv))) \/ (divset ((R_ (f . k)),x,(L_ x),Inv)) & (f . (k + 1)) `2 = ((R_ (f . k)) \/ (divset ((L_ (f . k)),x,(L_ x),Inv))) \/ (divset ((R_ (f . k)),x,(R_ x),Inv)) ) ; :: thesis:

end;

let T1, T2 be Function; :: thesis:
assume that
A2: ( dom T1 = omega & T1 . 0 = 1_No ) and
A3: for k being Nat holds
( T1 . k is pair & L_ (T1 . (k + 1)) = ((L_ (T1 . k)) \/ (divset ((L_ (T1 . k)),x,(R_ x),Inv))) \/ (divset ((R_ (T1 . k)),x,(L_ x),Inv)) & R_ (T1 . (k + 1)) = ((R_ (T1 . k)) \/ (divset ((L_ (T1 . k)),x,(L_ x),Inv))) \/ (divset ((R_ (T1 . k)),x,(R_ x),Inv)) ) and
A4: ( dom T2 = omega & T2 . 0 = 1_No ) and
A5: for k being Nat holds
( T2 . k is pair & L_ (T2 . (k + 1)) = ((L_ (T2 . k)) \/ (divset ((L_ (T2 . k)),x,(R_ x),Inv))) \/ (divset ((R_ (T2 . k)),x,(L_ x),Inv)) & R_ (T2 . (k + 1)) = ((R_ (T2 . k)) \/ (divset ((L_ (T2 . k)),x,(L_ x),Inv))) \/ (divset ((R_ (T2 . k)),x,(R_ x),Inv)) ) ; :: thesis:
defpred S₁[ Nat] means T1 . $1 = T2 . $1;
A6: S₁[ 0 ] by A2, A4;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A8: S₁[n] ; :: thesis:
A9: ( T1 . (n + 1) is pair & T2 . (n + 1) is pair ) by A3, A5;
R_ (T1 . (n + 1)) = ((R_ (T1 . n)) \/ (divset ((L_ (T1 . n)),x,(L_ x),Inv))) \/ (divset ((R_ (T1 . n)),x,(R_ x),Inv)) by A3;
then A10: (T1 . (n + 1)) `2 = R_ (T2 . (n + 1)) by A5, A8;
L_ (T1 . (n + 1)) = ((L_ (T1 . n)) \/ (divset ((L_ (T1 . n)),x,(R_ x),Inv))) \/ (divset ((R_ (T1 . n)),x,(L_ x),Inv)) by A3;
then (T1 . (n + 1)) `1 = (T2 . (n + 1)) `1 by A5, A8;
hence S₁[n + 1] by A9, A10, XTUPLE_0:2; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
then for o being object st o in dom T1 holds
T1 . o = T2 . o by A2;
hence T1 = T2 by A2, A4, FUNCT_1:2; :: thesis:

end;

:: deftheorem Def4 defines transitions_of SURREALI:def 4 :

definition

let x be object ;
let Inv be Function;

func divL (x,Inv) -> Function means :Def5: :: SURREALI:def 5
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x,Inv)) . k) `1 ) );

deffunc H₁( object ) -> object = ((transitions_of (x,Inv)) . $1) `1 ;
consider f being Function such that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis:
thus ( dom f = NAT & ( for k being Nat holds f . k = ((transitions_of (x,Inv)) . k) `1 ) ) by A1, A2, ORDINAL1:def 12; :: thesis:

end;

let D1, D2 be Function; :: thesis:
assume that
A3: ( dom D1 = NAT & ( for k being Nat holds D1 . k = ((transitions_of (x,Inv)) . k) `1 ) ) and
A4: ( dom D2 = NAT & ( for k being Nat holds D2 . k = ((transitions_of (x,Inv)) . k) `1 ) ) ; :: thesis:
for o being object st o in dom D1 holds
D1 . o = D2 . o

let o be object ; :: thesis:
assume o in dom D1 ; :: thesis:
then reconsider a = o as Nat by A3;
thus D1 . o = ((transitions_of (x,Inv)) . a) `1 by A3
.= D2 . o by A4 ; :: thesis:

end;

hence D1 = D2 by A3, A4, FUNCT_1:2; :: thesis:

end;

:: deftheorem Def5 defines divL SURREALI:def 5 :

definition

let x be object ;
let Inv be Function;

func divR (x,Inv) -> Function means :Def6: :: SURREALI:def 6
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x,Inv)) . k) `2 ) );

deffunc H₁( object ) -> object = ((transitions_of (x,Inv)) . $1) `2 ;
consider f being Function such that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis:
thus ( dom f = NAT & ( for k being Nat holds f . k = ((transitions_of (x,Inv)) . k) `2 ) ) by A1, A2, ORDINAL1:def 12; :: thesis:

end;

let D1, D2 be Function; :: thesis:
assume that
A3: ( dom D1 = NAT & ( for k being Nat holds D1 . k = ((transitions_of (x,Inv)) . k) `2 ) ) and
A4: ( dom D2 = NAT & ( for k being Nat holds D2 . k = ((transitions_of (x,Inv)) . k) `2 ) ) ; :: thesis:
for o being object st o in dom D1 holds
D1 . o = D2 . o

let o be object ; :: thesis:
assume o in dom D1 ; :: thesis:
then reconsider a = o as Nat by A3;
thus D1 . o = ((transitions_of (x,Inv)) . a) `2 by A3
.= D2 . o by A4 ; :: thesis:

end;

hence D1 = D2 by A3, A4, FUNCT_1:2; :: thesis:

end;

:: deftheorem Def6 defines divR SURREALI:def 6 :

registration

let a, b be Surreal;
let x, y be object ;

identify a * b with x *' y when a = x, b = y;

compatibility by Def1;

end;

theorem Th1: :: SURREALI:1

for o being object
for Inv being Function holds
( (divL (o,Inv)) . 0 = {0_No} & (divR (o,Inv)) . 0 = {} )

let o be object ; :: thesis:
let Inv be Function; :: thesis:
( (divL (o,Inv)) . 0 = L_ ((transitions_of (o,Inv)) . 0) & (divR (o,Inv)) . 0 = R_ ((transitions_of (o,Inv)) . 0) ) by Def5, Def6;
then ( (divL (o,Inv)) . 0 = L_ 1_No & (divR (o,Inv)) . 0 = R_ 1_No ) by Def4;
hence ( (divL (o,Inv)) . 0 = {0_No} & (divR (o,Inv)) . 0 = {} ) ; :: thesis:

end;

theorem :: SURREALI:2

for n, m being Nat
for o being object
for Inv being Function st n <= m holds
( (divL (o,Inv)) . n c= (divL (o,Inv)) . m & (divR (o,Inv)) . n c= (divR (o,Inv)) . m )

let n, m be Nat; :: thesis:
let o be object ; :: thesis:
let Inv be Function; :: thesis:
defpred S₁[ Nat] means ( (divL (o,Inv)) . n c= (divL (o,Inv)) . (n + $1) & (divR (o,Inv)) . n c= (divR (o,Inv)) . (n + $1) );
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

set T = transitions_of (o,Inv);
let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
set nk = n + k;
A4: ( (divL (o,Inv)) . ((n + k) + 1) = ((transitions_of (o,Inv)) . ((n + k) + 1)) `1 & (divR (o,Inv)) . ((n + k) + 1) = ((transitions_of (o,Inv)) . ((n + k) + 1)) `2 ) by Def5, Def6;
A5: ( (divL (o,Inv)) . (n + k) = L_ ((transitions_of (o,Inv)) . (n + k)) & (divR (o,Inv)) . (n + k) = R_ ((transitions_of (o,Inv)) . (n + k)) ) by Def5, Def6;
( ((transitions_of (o,Inv)) . ((n + k) + 1)) `1 = ((L_ ((transitions_of (o,Inv)) . (n + k))) \/ (divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv))) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv)) & ((transitions_of (o,Inv)) . ((n + k) + 1)) `2 = ((R_ ((transitions_of (o,Inv)) . (n + k))) \/ (divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv))) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv)) ) by Def4;
then ( ((transitions_of (o,Inv)) . ((n + k) + 1)) `1 = (L_ ((transitions_of (o,Inv)) . (n + k))) \/ ((divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv)) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv))) & ((transitions_of (o,Inv)) . ((n + k) + 1)) `2 = (R_ ((transitions_of (o,Inv)) . (n + k))) \/ ((divset ((L_ ((transitions_of (o,Inv)) . (n + k))),o,(L_ o),Inv)) \/ (divset ((R_ ((transitions_of (o,Inv)) . (n + k))),o,(R_ o),Inv))) ) by XBOOLE_1:4;
then ( L_ ((transitions_of (o,Inv)) . (n + k)) c= L_ ((transitions_of (o,Inv)) . ((n + k) + 1)) & R_ ((transitions_of (o,Inv)) . (n + k)) c= R_ ((transitions_of (o,Inv)) . ((n + k) + 1)) ) by XBOOLE_1:7;
hence S₁[k + 1] by A4, A5, A3, XBOOLE_1:1; :: thesis:

end;

A6: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
assume n <= m ; :: thesis:
then reconsider mn = m - n as Nat by NAT_1:21;
m = n + mn ;
hence ( (divL (o,Inv)) . n c= (divL (o,Inv)) . m & (divR (o,Inv)) . n c= (divR (o,Inv)) . m ) by A6; :: thesis:

end;

definition

let X be set ;
let f be Function;

attr f is X -surreal-valued means :: SURREALI:def 7
for o being object st o in X holds
f . o is Surreal;

end;

:: deftheorem defines -surreal-valued SURREALI:def 7 :

theorem :: SURREALI:3

for X, Y being set
for Inv being Function st Inv is Y -surreal-valued & X c= Y holds
Inv is X -surreal-valued ;

theorem Th4: :: SURREALI:4

for x, y being Surreal
for X being set
for Inv being Function holds divs (y,x,X,Inv) is surreal-membered

let x, y be Surreal; :: thesis:
let X be set ; :: thesis:
let Inv be Function; :: thesis:
let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in divs (y,x,X,Inv) ; :: thesis:
then ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' y)) *' (Inv . xL) ) by Def2;
hence o is surreal ; :: thesis:

end;

theorem Th5: :: SURREALI:5

for x being Surreal
for X, Y being set
for Inv being Function st Y is surreal-membered & X is surreal-membered & Inv is X -surreal-valued holds
divset (Y,x,X,Inv) is surreal-membered

let x be Surreal; :: thesis:
let X, Y be set ; :: thesis:
let Inv be Function; :: thesis:
assume A1: ( Y is surreal-membered & X is surreal-membered & Inv is X -surreal-valued ) ; :: thesis:
let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in divset (Y,x,X,Inv) ; :: thesis:
then consider l being object such that
A2: ( l in Y & o in divs (l,x,X,Inv) ) by Def3;
reconsider l = l as Surreal by A1, A2;
divs (l,x,X,Inv) is surreal-membered by Th4;
hence o is surreal by A2; :: thesis:

end;

theorem Th6: :: SURREALI:6

for n being Nat
for o being object
for Inv being Function holds
( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) )

let n be Nat; :: thesis:
let o be object ; :: thesis:
let Inv be Function; :: thesis:
set T = transitions_of (o,Inv);
A1: ( (divL (o,Inv)) . (n + 1) = ((transitions_of (o,Inv)) . (n + 1)) `1 & (divR (o,Inv)) . (n + 1) = ((transitions_of (o,Inv)) . (n + 1)) `2 ) by Def5, Def6;
( (divL (o,Inv)) . n = ((transitions_of (o,Inv)) . n) `1 & (divR (o,Inv)) . n = ((transitions_of (o,Inv)) . n) `2 ) by Def5, Def6;
hence ( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) ) by Def4, A1; :: thesis:

end;

theorem Th7: :: SURREALI:7

for o being object
for x being Surreal
for X being set
for Inv being Function holds divs (o,x,X,Inv) = divs (o,x,(X \ {0_No}),Inv)

let o be object ; :: thesis:
let x be Surreal; :: thesis:
let X be set ; :: thesis:
let Inv be Function; :: thesis:
thus divs (o,x,X,Inv) c= divs (o,x,(X \ {0_No}),Inv) :: according to XBOOLE_0:def 10 :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in divs (o,x,X,Inv) ; :: thesis:
then consider xL being object such that
A1: ( xL in X & xL <> 0_No & a = (1_No +' ((xL +' (-' x)) *' o)) *' (Inv . xL) ) by Def2;
xL in X \ {0_No} by A1, ZFMISC_1:56;
hence a in divs (o,x,(X \ {0_No}),Inv) by A1, Def2; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in divs (o,x,(X \ {0_No}),Inv) ; :: thesis:
then consider xL being object such that
A2: ( xL in X \ {0_No} & xL <> 0_No & a = (1_No +' ((xL +' (-' x)) *' o)) *' (Inv . xL) ) by Def2;
thus a in divs (o,x,X,Inv) by A2, Def2; :: thesis:

end;

theorem Th8: :: SURREALI:8

for x being Surreal
for X, Y being set
for Inv being Function holds divset (Y,x,X,Inv) = divset (Y,x,(X \ {0_No}),Inv)

let x be Surreal; :: thesis:
let X, Y be set ; :: thesis:
let Inv be Function; :: thesis:
thus divset (Y,x,X,Inv) c= divset (Y,x,(X \ {0_No}),Inv) :: according to XBOOLE_0:def 10 :: thesis:

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset (Y,x,X,Inv) ; :: thesis:
then consider lamb being object such that
A1: ( lamb in Y & o in divs (lamb,x,X,Inv) ) by Def3;
o in divs (lamb,x,(X \ {0_No}),Inv) by A1, Th7;
hence o in divset (Y,x,(X \ {0_No}),Inv) by A1, Def3; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset (Y,x,(X \ {0_No}),Inv) ; :: thesis:
then consider lamb being object such that
A2: ( lamb in Y & o in divs (lamb,x,(X \ {0_No}),Inv) ) by Def3;
o in divs (lamb,x,X,Inv) by A2, Th7;
hence o in divset (Y,x,X,Inv) by A2, Def3; :: thesis:

end;

theorem Th9: :: SURREALI:9

for n being Nat
for x being Surreal
for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered )

let n be Nat; :: thesis:
let x be Surreal; :: thesis:
let Inv be Function; :: thesis:
assume A1: Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued ; :: thesis:
defpred S₁[ Nat] means ( (divL (x,Inv)) . $1 is surreal-membered & (divR (x,Inv)) . $1 is surreal-membered );
{} is surreal-membered ;
then A2: S₁[ 0 ] by Th1;
A3: for m being Nat st S₁[m] holds
S₁[m + 1]

let m be Nat; :: thesis:
assume A4: S₁[m] ; :: thesis:
( (L_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} & (R_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} ) by XBOOLE_1:7, XBOOLE_1:33;
then A5: ( Inv is (L_ x) \ {0_No} -surreal-valued & Inv is (R_ x) \ {0_No} -surreal-valued ) by A1;
( divset (((divL (x,Inv)) . m),x,((L_ x) \ {0_No}),Inv) is surreal-membered & divset (((divL (x,Inv)) . m),x,((R_ x) \ {0_No}),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,((L_ x) \ {0_No}),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,((R_ x) \ {0_No}),Inv) is surreal-membered ) by A5, Th5, A4;
then A6: ( divset (((divL (x,Inv)) . m),x,(L_ x),Inv) is surreal-membered & divset (((divL (x,Inv)) . m),x,(R_ x),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,(L_ x),Inv) is surreal-membered & divset (((divR (x,Inv)) . m),x,(R_ x),Inv) is surreal-membered ) by Th8;
( (divL (x,Inv)) . (m + 1) = (((divL (x,Inv)) . m) \/ (divset (((divL (x,Inv)) . m),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . m),x,(L_ x),Inv)) & (divR (x,Inv)) . (m + 1) = (((divR (x,Inv)) . m) \/ (divset (((divL (x,Inv)) . m),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . m),x,(R_ x),Inv)) ) by Th6;
hence S₁[m + 1] by A4, A6; :: thesis:

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A3);
hence ( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered ) ; :: thesis:

end;

theorem Th10: :: SURREALI:10

for x being Surreal
for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( Union (divL (x,Inv)) is surreal-membered & Union (divR (x,Inv)) is surreal-membered )

let x be Surreal; :: thesis:
let Inv be Function; :: thesis:
assume A1: Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued ; :: thesis:
thus Union (divL (x,Inv)) is surreal-membered :: thesis:

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in Union (divL (x,Inv)) ; :: thesis:
then consider n being object such that
A2: ( n in dom (divL (x,Inv)) & o in (divL (x,Inv)) . n ) by CARD_5:2;
dom (divL (x,Inv)) = NAT by Def5;
then reconsider n = n as Nat by A2;
(divL (x,Inv)) . n is surreal-membered by Th9, A1;
hence o is surreal by A2; :: thesis:

end;

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in Union (divR (x,Inv)) ; :: thesis:
then consider n being object such that
A3: ( n in dom (divR (x,Inv)) & o in (divR (x,Inv)) . n ) by CARD_5:2;
dom (divR (x,Inv)) = NAT by Def6;
then reconsider n = n as Nat by A3;
(divR (x,Inv)) . n is surreal-membered by Th9, A1;
hence o is surreal by A3; :: thesis:

end;

theorem Th11: :: SURREALI:11

for x being Surreal
for X, Y, Z being set
for Inv being Function st Y c= Z holds
divset (Y,x,X,Inv) c= divset (Z,x,X,Inv)

let x be Surreal; :: thesis:
let X, Y, Z be set ; :: thesis:
let Inv be Function; :: thesis:
assume A1: Y c= Z ; :: thesis:
let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset (Y,x,X,Inv) ; :: thesis:
then ex lamb being object st
( lamb in Y & o in divs (lamb,x,X,Inv) ) by Def3;
hence o in divset (Z,x,X,Inv) by A1, Def3; :: thesis:

end;

theorem Th12: :: SURREALI:12

for x being Surreal
for Inv being Function holds Union (divL (x,Inv)) = ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))

let x be Surreal; :: thesis:
let Inv be Function; :: thesis:
defpred S₁[ Nat] means (divL (x,Inv)) . $1 c= ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv));
(divL (x,Inv)) . 0 = {0_No} by Th1;
then A1: S₁[ 0 ] by XBOOLE_1:7, XBOOLE_1:10;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: o in (divL (x,Inv)) . (n + 1) ; :: thesis:
(divL (x,Inv)) . (n + 1) = (((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(L_ x),Inv)) by Th6;
then ( o in ((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv)) or o in divset (((divR (x,Inv)) . n),x,(L_ x),Inv) ) by A4, XBOOLE_0:def 3;

suppose o in (divL (x,Inv)) . n ; :: thesis:

hence o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) by A3; :: thesis:

end;

suppose A5: o in divset (((divL (x,Inv)) . n),x,(R_ x),Inv) ; :: thesis:

divset (((divL (x,Inv)) . n),x,(R_ x),Inv) c= divset ((Union (divL (x,Inv))),x,(R_ x),Inv) by ABCMIZ_1:1, Th11;
then o in {0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv)) by A5, XBOOLE_0:def 3;
hence o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) by XBOOLE_0:def 3; :: thesis:

end;

suppose A6: o in divset (((divR (x,Inv)) . n),x,(L_ x),Inv) ; :: thesis:

divset (((divR (x,Inv)) . n),x,(L_ x),Inv) c= divset ((Union (divR (x,Inv))),x,(L_ x),Inv) by Th11, ABCMIZ_1:1;
hence o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) by A6, XBOOLE_0:def 3; :: thesis:

end;

A7: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
thus Union (divL (x,Inv)) c= ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) :: according to XBOOLE_0:def 10 :: thesis:

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in Union (divL (x,Inv)) ; :: thesis:
then consider n being object such that
A8: ( n in dom (divL (x,Inv)) & o in (divL (x,Inv)) . n ) by CARD_5:2;
n in NAT by A8, Def5;
then reconsider n = n as Nat ;
(divL (x,Inv)) . n c= ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) by A7;
hence o in ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) by A8; :: thesis:

end;

A9: divset ((Union (divL (x,Inv))),x,(R_ x),Inv) c= Union (divL (x,Inv))

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset ((Union (divL (x,Inv))),x,(R_ x),Inv) ; :: thesis:
then consider l being object such that
A10: ( l in Union (divL (x,Inv)) & o in divs (l,x,(R_ x),Inv) ) by Def3;
consider n being object such that
A11: ( n in dom (divL (x,Inv)) & l in (divL (x,Inv)) . n ) by A10, CARD_5:2;
n in NAT by A11, Def5;
then reconsider n = n as Nat ;
o in divset (((divL (x,Inv)) . n),x,(R_ x),Inv) by A10, A11, Def3;
then o in ((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv)) by XBOOLE_0:def 3;
then o in (((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(L_ x),Inv)) by XBOOLE_0:def 3;
then A12: o in (divL (x,Inv)) . (n + 1) by Th6;
n + 1 in NAT ;
then n + 1 in dom (divL (x,Inv)) by Def5;
hence o in Union (divL (x,Inv)) by A12, CARD_5:2; :: thesis:

end;

A13: divset ((Union (divR (x,Inv))),x,(L_ x),Inv) c= Union (divL (x,Inv))

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset ((Union (divR (x,Inv))),x,(L_ x),Inv) ; :: thesis:
then consider l being object such that
A14: ( l in Union (divR (x,Inv)) & o in divs (l,x,(L_ x),Inv) ) by Def3;
consider n being object such that
A15: ( n in dom (divR (x,Inv)) & l in (divR (x,Inv)) . n ) by A14, CARD_5:2;
n in NAT by A15, Def6;
then reconsider n = n as Nat ;
o in divset (((divR (x,Inv)) . n),x,(L_ x),Inv) by A14, A15, Def3;
then o in (((divL (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(R_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(L_ x),Inv)) by XBOOLE_0:def 3;
then A16: o in (divL (x,Inv)) . (n + 1) by Th6;
n + 1 in NAT ;
then n + 1 in dom (divL (x,Inv)) by Def5;
hence o in Union (divL (x,Inv)) by A16, CARD_5:2; :: thesis:

end;

(divL (x,Inv)) . 0 = {0_No} by Th1;
then {0_No} c= Union (divL (x,Inv)) by ABCMIZ_1:1;
then {0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv)) c= Union (divL (x,Inv)) by A9, XBOOLE_1:8;
hence ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv)) c= Union (divL (x,Inv)) by A13, XBOOLE_1:8; :: thesis:

end;

theorem Th13: :: SURREALI:13

for x being Surreal
for Inv being Function holds Union (divR (x,Inv)) = (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))

let x be Surreal; :: thesis:
let Inv be Function; :: thesis:
defpred S₁[ Nat] means (divR (x,Inv)) . $1 c= (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv));
(divR (x,Inv)) . 0 = {} by Th1;
then A1: S₁[ 0 ] by XBOOLE_1:2;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: o in (divR (x,Inv)) . (n + 1) ; :: thesis:
(divR (x,Inv)) . (n + 1) = (((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(R_ x),Inv)) by Th6;
then ( o in ((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv)) or o in divset (((divR (x,Inv)) . n),x,(R_ x),Inv) ) by A4, XBOOLE_0:def 3;

suppose o in (divR (x,Inv)) . n ; :: thesis:

hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A3; :: thesis:

end;

suppose A5: o in divset (((divL (x,Inv)) . n),x,(L_ x),Inv) ; :: thesis:

divset (((divL (x,Inv)) . n),x,(L_ x),Inv) c= divset ((Union (divL (x,Inv))),x,(L_ x),Inv) by Th11, ABCMIZ_1:1;
hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A5, XBOOLE_0:def 3; :: thesis:

end;

suppose A6: o in divset (((divR (x,Inv)) . n),x,(R_ x),Inv) ; :: thesis:

divset (((divR (x,Inv)) . n),x,(R_ x),Inv) c= divset ((Union (divR (x,Inv))),x,(R_ x),Inv) by Th11, ABCMIZ_1:1;
hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A6, XBOOLE_0:def 3; :: thesis:

end;

A7: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
thus Union (divR (x,Inv)) c= (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) :: according to XBOOLE_0:def 10 :: thesis:

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in Union (divR (x,Inv)) ; :: thesis:
then consider n being object such that
A8: ( n in dom (divR (x,Inv)) & o in (divR (x,Inv)) . n ) by CARD_5:2;
n in NAT by A8, Def6;
then reconsider n = n as Nat ;
(divR (x,Inv)) . n c= (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A7;
hence o in (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) by A8; :: thesis:

end;

A9: divset ((Union (divL (x,Inv))),x,(L_ x),Inv) c= Union (divR (x,Inv))

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset ((Union (divL (x,Inv))),x,(L_ x),Inv) ; :: thesis:
then consider l being object such that
A10: ( l in Union (divL (x,Inv)) & o in divs (l,x,(L_ x),Inv) ) by Def3;
consider n being object such that
A11: ( n in dom (divL (x,Inv)) & l in (divL (x,Inv)) . n ) by A10, CARD_5:2;
n in NAT by A11, Def5;
then reconsider n = n as Nat ;
o in divset (((divL (x,Inv)) . n),x,(L_ x),Inv) by A10, A11, Def3;
then o in ((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv)) by XBOOLE_0:def 3;
then o in (((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(R_ x),Inv)) by XBOOLE_0:def 3;
then A12: o in (divR (x,Inv)) . (n + 1) by Th6;
n + 1 in NAT ;
then n + 1 in dom (divR (x,Inv)) by Def6;
hence o in Union (divR (x,Inv)) by A12, CARD_5:2; :: thesis:

end;

divset ((Union (divR (x,Inv))),x,(R_ x),Inv) c= Union (divR (x,Inv))

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset ((Union (divR (x,Inv))),x,(R_ x),Inv) ; :: thesis:
then consider l being object such that
A13: ( l in Union (divR (x,Inv)) & o in divs (l,x,(R_ x),Inv) ) by Def3;
consider n being object such that
A14: ( n in dom (divR (x,Inv)) & l in (divR (x,Inv)) . n ) by A13, CARD_5:2;
n in NAT by A14, Def6;
then reconsider n = n as Nat ;
o in divset (((divR (x,Inv)) . n),x,(R_ x),Inv) by A13, A14, Def3;
then o in (((divR (x,Inv)) . n) \/ (divset (((divL (x,Inv)) . n),x,(L_ x),Inv))) \/ (divset (((divR (x,Inv)) . n),x,(R_ x),Inv)) by XBOOLE_0:def 3;
then A15: o in (divR (x,Inv)) . (n + 1) by Th6;
n + 1 in NAT ;
then n + 1 in dom (divR (x,Inv)) by Def6;
hence o in Union (divR (x,Inv)) by A15, CARD_5:2; :: thesis:

end;

hence (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv)) c= Union (divR (x,Inv)) by A9, XBOOLE_1:8; :: thesis:

end;

theorem Th14: :: SURREALI:14

for a, b being object
for X, Z being set
for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divs (a,b,X,I1) = divs (a,b,X,I2)

let a, b be object ; :: thesis:
let X, Z be set ; :: thesis:
let I1, I2 be Function; :: thesis:
assume A1: ( X \ {0_No} c= Z & I1 | Z = I2 | Z ) ; :: thesis:
thus divs (a,b,X,I1) c= divs (a,b,X,I2) :: according to XBOOLE_0:def 10 :: thesis:

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divs (a,b,X,I1) ; :: thesis:
then consider xL being object such that
A2: ( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' b)) *' a)) *' (I1 . xL) ) by Def2;
A3: xL in X \ {0_No} by A2, ZFMISC_1:56;
then I1 . xL = (I2 | Z) . xL by A1, FUNCT_1:49
.= I2 . xL by A3, A1, FUNCT_1:49 ;
hence o in divs (a,b,X,I2) by A2, Def2; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divs (a,b,X,I2) ; :: thesis:
then consider xL being object such that
A4: ( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' b)) *' a)) *' (I2 . xL) ) by Def2;
A5: xL in X \ {0_No} by A4, ZFMISC_1:56;
then I2 . xL = (I1 | Z) . xL by A1, FUNCT_1:49
.= I1 . xL by A5, A1, FUNCT_1:49 ;
hence o in divs (a,b,X,I1) by A4, Def2; :: thesis:

end;

theorem Th15: :: SURREALI:15

for o being object
for X, Y, Z being set
for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divset (Y,o,X,I1) = divset (Y,o,X,I2)

let o be object ; :: thesis:
let X, Y, Z be set ; :: thesis:
let I1, I2 be Function; :: thesis:
assume A1: ( X \ {0_No} c= Z & I1 | Z = I2 | Z ) ; :: thesis:
thus divset (Y,o,X,I1) c= divset (Y,o,X,I2) :: according to XBOOLE_0:def 10 :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in divset (Y,o,X,I1) ; :: thesis:
then consider lamb being object such that
A2: ( lamb in Y & a in divs (lamb,o,X,I1) ) by Def3;
divs (lamb,o,X,I1) = divs (lamb,o,X,I2) by A1, Th14;
hence a in divset (Y,o,X,I2) by A2, Def3; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in divset (Y,o,X,I2) ; :: thesis:
then consider lamb being object such that
A3: ( lamb in Y & a in divs (lamb,o,X,I2) ) by Def3;
divs (lamb,o,X,I1) = divs (lamb,o,X,I2) by A1, Th14;
hence a in divset (Y,o,X,I1) by A3, Def3; :: thesis:

end;

theorem Th16: :: SURREALI:16

for Z being set
for I1, I2 being Function
for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
transitions_of (x,I1) = transitions_of (x,I2)

let Z be set ; :: thesis:
let I1, I2 be Function; :: thesis:
let x be object ; :: thesis:
assume A1: ( ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z ) ; :: thesis:
set T1 = transitions_of (x,I1);
set T2 = transitions_of (x,I2);
defpred S₁[ Nat] means (transitions_of (x,I1)) . $1 = (transitions_of (x,I2)) . $1;
(transitions_of (x,I1)) . 0 = 1_No by Def4;
then A2: S₁[ 0 ] by Def4;
A3: ( (L_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} & (R_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} ) by XBOOLE_1:7, XBOOLE_1:33;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A5: S₁[n] ; :: thesis:
A6: ( (transitions_of (x,I1)) . (n + 1) is pair & (transitions_of (x,I2)) . (n + 1) is pair ) by Def4;
A7: ((transitions_of (x,I1)) . (n + 1)) `1 = ((L_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(R_ x),I1))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1)) by Def4
.= ((L_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(R_ x),I2))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1)) by A1, A3, XBOOLE_1:1, Th15
.= ((L_ ((transitions_of (x,I2)) . n)) \/ (divset ((L_ ((transitions_of (x,I2)) . n)),x,(R_ x),I2))) \/ (divset ((R_ ((transitions_of (x,I2)) . n)),x,(L_ x),I2)) by A1, A3, XBOOLE_1:1, Th15, A5
.= ((transitions_of (x,I2)) . (n + 1)) `1 by Def4 ;
((transitions_of (x,I1)) . (n + 1)) `2 = ((R_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(R_ x),I1)) by Def4
.= ((R_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(R_ x),I2)) by A1, A3, XBOOLE_1:1, Th15
.= ((R_ ((transitions_of (x,I2)) . n)) \/ (divset ((L_ ((transitions_of (x,I2)) . n)),x,(L_ x),I2))) \/ (divset ((R_ ((transitions_of (x,I2)) . n)),x,(R_ x),I2)) by A1, A3, XBOOLE_1:1, Th15, A5
.= ((transitions_of (x,I2)) . (n + 1)) `2 by Def4 ;
hence S₁[n + 1] by A6, A7, XTUPLE_0:2; :: thesis:

end;

A8: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A4);
A9: ( dom (transitions_of (x,I1)) = NAT & NAT = dom (transitions_of (x,I2)) ) by Def4;
then for o being object st o in dom (transitions_of (x,I1)) holds
(transitions_of (x,I1)) . o = (transitions_of (x,I2)) . o by A8;
hence transitions_of (x,I1) = transitions_of (x,I2) by A9, FUNCT_1:2; :: thesis:

end;

theorem Th17: :: SURREALI:17

for Z being set
for I1, I2 being Function
for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
( divL (x,I1) = divL (x,I2) & divR (x,I1) = divR (x,I2) )

let Z be set ; :: thesis:
let I1, I2 be Function; :: thesis:
let x be object ; :: thesis:
assume A1: ( ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z ) ; :: thesis:
A2: transitions_of (x,I1) = transitions_of (x,I2) by A1, Th16;
A3: ( dom (divL (x,I1)) = NAT & NAT = dom (divL (x,I2)) ) by Def5;
for o being object st o in dom (divL (x,I1)) holds
(divL (x,I1)) . o = (divL (x,I2)) . o

let o be object ; :: thesis:
assume o in dom (divL (x,I1)) ; :: thesis:
then reconsider n = o as Nat by A3;
thus (divL (x,I1)) . o = ((transitions_of (x,I1)) . n) `1 by Def5
.= (divL (x,I2)) . o by A2, Def5 ; :: thesis:

end;

hence divL (x,I1) = divL (x,I2) by A3, FUNCT_1:2; :: thesis:
A4: ( dom (divR (x,I1)) = NAT & NAT = dom (divR (x,I2)) ) by Def6;
for o being object st o in dom (divR (x,I1)) holds
(divR (x,I1)) . o = (divR (x,I2)) . o

let o be object ; :: thesis:
assume o in dom (divR (x,I1)) ; :: thesis:
then reconsider n = o as Nat by A4;
thus (divR (x,I1)) . o = ((transitions_of (x,I1)) . n) `2 by Def6
.= (divR (x,I2)) . o by Def6, A2 ; :: thesis:

end;

hence divR (x,I1) = divR (x,I2) by A4, FUNCT_1:2; :: thesis:

end;

definition

let x be Surreal;

attr x is positive means :Def8: :: SURREALI:def 8
0_No < x;

end;

:: deftheorem Def8 defines positive SURREALI:def 8 :

registration

cluster 1_No -> positive ;

A1: 0_No in {0_No} by TARSKI:def 1;
assume 1_No <= 0_No ; :: according to SURREALI:def 8 :: thesis:
then L_ 1_No << {0_No} by SURREAL0:43;
hence contradiction by SURREALO:3, A1; :: thesis:

end;

registration

cluster non empty pair surreal positive for set ;

take 1_No ; :: thesis:
thus 1_No is positive ; :: thesis:

end;

registration

let x, y be positive Surreal;

cluster x + y -> positive ;

( 0_No < x & 0_No <= y ) by Def8;
then 0_No + 0_No < x + y by SURREALR:44;
hence x + y is positive ; :: thesis:

end;

cluster x * y -> positive ;

( 0_No < x & 0_No < y ) by Def8;
hence x * y is positive by SURREALR:72; :: thesis:

end;

let x be Surreal; :: thesis:
assume A1: 0_No < x ; :: thesis:
defpred S₁[ object ] means for z being Surreal st z = $1 holds
0_No < z;
consider yL being set such that
A2: for o being object holds
( o in yL iff ( o in L_ x & S₁[o] ) ) from XBOOLE_0:sch 1();
consider yR being set such that
A3: for o being object holds
( o in yR iff ( o in R_ x & S₁[o] ) ) from XBOOLE_0:sch 1();
set YL = yL \/ {0_No};
A4: yL \/ {0_No} << yR

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A5: ( l in yL \/ {0_No} & r in yR ) ; :: thesis:

per cases by A5, ZFMISC_1:136;

suppose A6: l in yL ; :: thesis:

A7: L_ x << R_ x by SURREAL0:45;
( l in L_ x & r in R_ x ) by A6, A5, A2, A3;
hence not r <= l by A7; :: thesis:

end;

suppose l = 0_No ; :: thesis:

hence not r <= l by A3, A5; :: thesis:

end;

A8: for o being object st o in (yL \/ {0_No}) \/ yR holds
ex O being Ordinal st
( O in born x & o in Day O )

let o be object ; :: thesis:
assume o in (yL \/ {0_No}) \/ yR ; :: thesis:
then ( o in yL \/ {0_No} or o in yR ) by XBOOLE_0:def 3;
then A9: ( o in yL or o = 0_No or o in yR ) by ZFMISC_1:136;
then reconsider o = o as Surreal by SURREAL0:def 16, A2, A3;
take born o ; :: thesis:
0_No <= 0_No ;
then born x <> {} by A1, SURREAL0:37;
then {} c< born x by XBOOLE_1:2, XBOOLE_0:def 8;
then A10: {} in born x by ORDINAL1:11;
( o in L_ x or o = 0_No or o in R_ x ) by A9, A2, A3;
then ( o in (L_ x) \/ (R_ x) or o = 0_No ) by XBOOLE_0:def 3;
hence ( born o in born x & o in Day (born o) ) by SURREAL0:def 18, A10, SURREAL0:37, SURREALO:1; :: thesis:

end;

[(yL \/ {0_No}),yR] in Day (born x) by A4, A8, SURREAL0:46;
then reconsider y = [(yL \/ {0_No}),yR] as Surreal ;
take y ; :: thesis:
A11: x = [(L_ x),(R_ x)] ;
A12: for a being Surreal st a in yL \/ {0_No} holds
ex b being Surreal st
( b in L_ x & a <= b )

let a be Surreal; :: thesis:
( ex xR being Surreal st
( xR in R_ 0_No & 0_No < xR & xR <= x ) or ex yL being Surreal st
( yL in L_ x & 0_No <= yL & yL < x ) ) by A1, SURREALO:13;
then consider L being Surreal such that
A13: ( L in L_ x & 0_No <= L & L < x ) ;
assume a in yL \/ {0_No} ; :: thesis:
then ( a in yL or a = 0_No ) by ZFMISC_1:136;
hence ex b being Surreal st
( b in L_ x & a <= b ) by A13, A2; :: thesis:

end;

A14: for a being Surreal st a in R_ x holds
ex b being Surreal st
( b in yR & b <= a )

let a be Surreal; :: thesis:
assume A15: a in R_ x ; :: thesis:
0_No <= x by A1;
then ( 0_No in {0_No} & {0_No} << R_ x ) by SURREAL0:43, TARSKI:def 1;
then S₁[a] by A15;
hence ex b being Surreal st
( b in yR & b <= a ) by A15, A3; :: thesis:

end;

A16: for a being Surreal st a in yR holds
ex b being Surreal st
( b in R_ x & b <= a ) by A3;
for a being Surreal st a in L_ x holds
ex b being Surreal st
( b in yL \/ {0_No} & a <= b )

let a be Surreal; :: thesis:
assume A17: a in L_ x ; :: thesis:

suppose 0_No < a ; :: thesis:

then S₁[a] ;
then a in yL \/ {0_No} by A2, A17, ZFMISC_1:136;
hence ex b being Surreal st
( b in yL \/ {0_No} & a <= b ) ; :: thesis:

end;

suppose A18: a <= 0_No ; :: thesis:

0_No in yL \/ {0_No} by ZFMISC_1:136;
hence ex b being Surreal st
( b in yL \/ {0_No} & a <= b ) by A18; :: thesis:

end;

hence y == x by A14, A12, SURREAL0:44, A16, A11; :: thesis:
thus for z being Surreal holds
( z in L_ y iff ( z = 0_No or ( z in L_ x & 0_No < z ) ) ) :: thesis:

let z be Surreal; :: thesis:
thus ( not z in L_ y or z = 0_No or ( z in L_ x & 0_No < z ) ) :: thesis:

assume ( z in L_ y & z <> 0_No ) ; :: thesis:
then z in yL by ZFMISC_1:136;
hence ( z in L_ x & 0_No < z ) by A2; :: thesis:

end;

assume A19: ( z = 0_No or ( z in L_ x & 0_No < z ) ) ; :: thesis:
assume A20: not z in L_ y ; :: thesis:
then S₁[z] by A19, ZFMISC_1:136;
hence contradiction by A20, A19, A2, ZFMISC_1:136; :: thesis:

end;

let z be Surreal; :: thesis:
thus ( z in R_ y implies ( z in R_ x & 0_No < z ) ) by A3; :: thesis:
assume A21: ( z in R_ x & 0_No < z ) ; :: thesis:
then S₁[z] ;
hence z in R_ y by A3, A21; :: thesis:

end;

definition

let x be object ;
assume A1: x is positive Surreal ;

func ||.x.|| -> positive Surreal means :Def9: :: SURREALI:def 9
for y being Surreal holds
( ( not y in L_ it or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ it ) & ( y in R_ it implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ it ) );

reconsider X = x as Surreal by A1;
consider s being Surreal such that
A2: s == X and
A3: for z being Surreal holds
( z in L_ s iff ( z = 0_No or ( z in L_ x & 0_No < z ) ) ) and
A4: for z being Surreal holds
( z in R_ s iff ( z in R_ x & 0_No < z ) ) by Lm1, A1, Def8;
0_No < s by A2, A1, Def8, SURREALO:4;
then reconsider s = s as positive Surreal by Def8;
take s ; :: thesis:
thus for y being Surreal holds
( ( not y in L_ s or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s ) & ( y in R_ s implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s ) ) by A3, A4; :: thesis:

end;

let s1, s2 be positive Surreal; :: thesis:
assume that
A5: for y being Surreal holds
( ( not y in L_ s1 or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s1 ) & ( y in R_ s1 implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s1 ) ) and
A6: for y being Surreal holds
( ( not y in L_ s2 or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s2 ) & ( y in R_ s2 implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s2 ) ) ; :: thesis:
for o being object st o in L_ s1 holds
o in L_ s2

let o be object ; :: thesis:
assume A7: o in L_ s1 ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ x & o is positive ) ) by A7, A5;
hence o in L_ s2 by A6; :: thesis:

end;

then A8: L_ s1 c= L_ s2 by TARSKI:def 3;
for o being object st o in L_ s2 holds
o in L_ s1

let o be object ; :: thesis:
assume A9: o in L_ s2 ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ x & o is positive ) ) by A9, A6;
hence o in L_ s1 by A5; :: thesis:

end;

then L_ s2 c= L_ s1 by TARSKI:def 3;
then A10: L_ s1 = L_ s2 by A8, XBOOLE_0:def 10;
for o being object st o in R_ s1 holds
o in R_ s2

let o be object ; :: thesis:
assume A11: o in R_ s1 ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ x & o is positive ) by A11, A5;
hence o in R_ s2 by A6; :: thesis:

end;

then A12: R_ s1 c= R_ s2 by TARSKI:def 3;
for o being object st o in R_ s2 holds
o in R_ s1

let o be object ; :: thesis:
assume A13: o in R_ s2 ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ x & o is positive ) by A13, A6;
hence o in R_ s1 by A5; :: thesis:

end;

then R_ s2 c= R_ s1 by TARSKI:def 3;
then R_ s1 = R_ s2 by A12, XBOOLE_0:def 10;
hence s1 = s2 by A10, XTUPLE_0:2; :: thesis:

end;

:: deftheorem Def9 defines ||. SURREALI:def 9 :

theorem Th18: :: SURREALI:18

for x being Surreal st x is positive holds
x == ||.x.||

let x be Surreal; :: thesis:
assume A1: x is positive ; :: thesis:
then consider y being Surreal such that
A2: y == x and
A3: for z being Surreal holds
( z in L_ y iff ( z = 0_No or ( z in L_ x & 0_No < z ) ) ) and
A4: for z being Surreal holds
( z in R_ y iff ( z in R_ x & 0_No < z ) ) by Lm1;
0_No < y by A1, A2, SURREALO:4;
then reconsider y = y as positive Surreal by Def8;
for z being Surreal holds
( ( not z in L_ y or z = 0_No or ( z in L_ x & z is positive ) ) & ( ( z = 0_No or ( z in L_ x & z is positive ) ) implies z in L_ y ) & ( z in R_ y implies ( z in R_ x & z is positive ) ) & ( z in R_ x & z is positive implies z in R_ y ) ) by A3, A4;
hence x == ||.x.|| by A2, A1, Def9; :: thesis:

end;

theorem :: SURREALI:19

for x being Surreal st x is positive holds
||.||.x.||.|| = ||.x.||

let x be Surreal; :: thesis:
set Nx = ||.x.||;
set NNx = ||.||.x.||.||;
assume A1: x is positive ; :: thesis:
for o being object st o in L_ ||.||.x.||.|| holds
o in L_ ||.x.||

let o be object ; :: thesis:
assume A2: ( o in L_ ||.||.x.||.|| & not o in L_ ||.x.|| ) ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ ||.x.|| & o is positive ) ) by A2, Def9;
hence contradiction by A1, A2, Def9; :: thesis:

end;

then A3: L_ ||.||.x.||.|| c= L_ ||.x.|| by TARSKI:def 3;
for o being object st o in L_ ||.x.|| holds
o in L_ ||.||.x.||.||

let o be object ; :: thesis:
assume A4: ( o in L_ ||.x.|| & not o in L_ ||.||.x.||.|| ) ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ x & o is positive ) ) by A1, A4, Def9;
hence contradiction by A4, Def9; :: thesis:

end;

then L_ ||.x.|| c= L_ ||.||.x.||.|| by TARSKI:def 3;
then A5: L_ ||.x.|| = L_ ||.||.x.||.|| by A3, XBOOLE_0:def 10;
for o being object st o in R_ ||.||.x.||.|| holds
o in R_ ||.x.||

let o be object ; :: thesis:
assume A6: ( o in R_ ||.||.x.||.|| & not o in R_ ||.x.|| ) ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ ||.x.|| & o is positive ) by A6, Def9;
hence contradiction by A6; :: thesis:

end;

then A7: R_ ||.||.x.||.|| c= R_ ||.x.|| by TARSKI:def 3;
for o being object st o in R_ ||.x.|| holds
o in R_ ||.||.x.||.||

let o be object ; :: thesis:
assume A8: ( o in R_ ||.x.|| & not o in R_ ||.||.x.||.|| ) ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ x & o is positive ) by A1, A8, Def9;
hence contradiction by A8, Def9; :: thesis:

end;

then R_ ||.x.|| c= R_ ||.||.x.||.|| by TARSKI:def 3;
then R_ ||.x.|| = R_ ||.||.x.||.|| by A7, XBOOLE_0:def 10;
hence ||.||.x.||.|| = ||.x.|| by A5, XTUPLE_0:2; :: thesis:

end;

theorem Th20: :: SURREALI:20

for x being Surreal st x is positive holds
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x)

let x be Surreal; :: thesis:
assume A1: x is positive ; :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider a = a as Surreal by SURREAL0:def 16;
A3: ( a in (L_ ||.x.||) \/ (R_ ||.x.||) & a <> 0_No ) by A2, ZFMISC_1:56;
( a in L_ ||.x.|| or a in R_ ||.x.|| ) by A2, XBOOLE_0:def 3;
then ( a in L_ x or a in R_ x ) by Def9, A1, A3;
hence a in (L_ x) \/ (R_ x) by XBOOLE_0:def 3; :: thesis:

end;

theorem Th21: :: SURREALI:21

for x, y being Surreal st x is positive & y in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} holds
y is positive

let x, y be Surreal; :: thesis:
assume A1: ( x is positive & y in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ) ; :: thesis:
then A2: ( y in (L_ ||.x.||) \/ (R_ ||.x.||) & y <> 0_No ) by ZFMISC_1:56;
( y in L_ ||.x.|| or y in R_ ||.x.|| ) by A1, XBOOLE_0:def 3;
hence y is positive by Def9, A1, A2; :: thesis:

end;

theorem Th22: :: SURREALI:22

for x being Surreal st x is positive holds
born ||.x.|| c= born x

let x be Surreal; :: thesis:
A1: 0_No <= 0_No ;
assume A2: x is positive ; :: thesis:
then A3: {} in born x by A1, SURREAL0:37, ORDINAL3:8;
A4: born 0_No = {} by SURREAL0:37;
set Nx = ||.x.||;
for o being object st o in (L_ ||.x.||) \/ (R_ ||.x.||) holds
ex O being Ordinal st
( O in born x & o in Day O )

let o be object ; :: thesis:
assume A5: o in (L_ ||.x.||) \/ (R_ ||.x.||) ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;

suppose o = 0_No ; :: thesis:

then o in Day {} by SURREAL0:def 18, A4;
hence ex O being Ordinal st
( O in born x & o in Day O ) by A3; :: thesis:

end;

suppose o <> 0_No ; :: thesis:

then A6: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A5, ZFMISC_1:56;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A2, Th20;
then ( born o in born x & o in Day (born o) ) by A6, SURREALO:1, SURREAL0:def 18;
hence ex O being Ordinal st
( O in born x & o in Day O ) ; :: thesis:

end;

then ( ||.x.|| = [(L_ ||.x.||),(R_ ||.x.||)] & [(L_ ||.x.||),(R_ ||.x.||)] in Day (born x) ) by SURREAL0:45, SURREAL0:46;
hence born ||.x.|| c= born x by SURREAL0:def 18; :: thesis:

end;

definition

let A be Ordinal;

func Positives A -> Subset of (Day A) means :Def10: :: SURREALI:def 10
for x being Surreal holds
( x in it iff ( x in Day A & 0_No < x ) );

defpred S₁[ object ] means for y being Surreal st y = $1 holds
0_No < y;
consider P being set such that
A1: for o being object holds
( o in P iff ( o in Day A & S₁[o] ) ) from XBOOLE_0:sch 1();
P c= Day A

let o be object ; :: according to TARSKI:def 3 :: thesis:
thus ( not o in P or o in Day A ) by A1; :: thesis:

end;

then reconsider P = P as Subset of (Day A) ;
take P ; :: thesis:
let x be Surreal; :: thesis:
thus ( x in P implies ( x in Day A & 0_No < x ) ) by A1; :: thesis:
assume A2: ( x in Day A & 0_No < x ) ; :: thesis:
then S₁[x] ;
hence x in P by A2, A1; :: thesis:

end;

let P1, P2 be Subset of (Day A); :: thesis:
assume that
A3: for x being Surreal holds
( x in P1 iff ( x in Day A & 0_No < x ) ) and
A4: for x being Surreal holds
( x in P2 iff ( x in Day A & 0_No < x ) ) ; :: thesis:
for o being object st o in P1 holds
o in P2

let o be object ; :: thesis:
assume A5: o in P1 ; :: thesis:
then reconsider x = o as Surreal ;
( x in Day A & 0_No < x ) by A3, A5;
hence o in P2 by A4; :: thesis:

end;

then A6: P1 c= P2 by TARSKI:def 3;
for o being object st o in P2 holds
o in P1

let o be object ; :: thesis:
assume A7: o in P2 ; :: thesis:
then reconsider x = o as Surreal ;
( x in Day A & 0_No < x ) by A4, A7;
hence o in P1 by A3; :: thesis:

end;

then P2 c= P1 by TARSKI:def 3;
hence P1 = P2 by A6, XBOOLE_0:def 10; :: thesis:

end;

:: deftheorem Def10 defines Positives SURREALI:def 10 :

theorem Th23: :: SURREALI:23

for A, B being Ordinal st A c= B holds
Positives A c= Positives B

let A, B be Ordinal; :: thesis:
assume A1: A c= B ; :: thesis:
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A2: [x,y] in Positives A ; :: thesis:
then reconsider xy = [x,y] as Surreal ;
( xy in Day A & Day A c= Day B & 0_No < xy ) by A1, A2, Def10, SURREAL0:35;
hence [x,y] in Positives B by Def10; :: thesis:

end;

theorem Th24: :: SURREALI:24

for x being Surreal st x is positive holds
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x)

let x be Surreal; :: thesis:
assume A1: x is positive ; :: thesis:
A2: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A1, Th20;
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider a = a as Surreal by SURREAL0:def 16;
A4: a is positive by A1, A3, Th21;
born a in born x by A3, A2, SURREALO:1;
then ( a in Day (born a) & Day (born a) c= Day (born x) ) by SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;
hence a in Positives (born x) by A4, Def10; :: thesis:

end;

definition

let A be Ordinal;

func No_inverse_op A -> ManySortedSet of Positives A means :Def11: :: SURREALI:def 11
ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & it = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) );

deffunc H₁( Ordinal) -> Subset of (Day $1) = Positives $1;
A1: for A, B being Ordinal st A c= B holds
H₁(A) c= H₁(B) by Th23;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (divL (||.$1.||,(union (rng $2))))),(Union (divR (||.$1.||,(union (rng $2)))))];
A2: for S being c=-monotone Function-yielding Sequence st ( for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ) holds
for A being Ordinal
for o being object st o in dom (S . A) holds
H₂(o,S | A) = H₂(o,S)

let S be c=-monotone Function-yielding Sequence; :: thesis:
assume A3: for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ; :: thesis:
let A be Ordinal; :: thesis:
let o be object ; :: thesis:
assume A4: o in dom (S . A) ; :: thesis:
S . A <> {} by A4;
then A5: A in dom S by FUNCT_1:def 2;
then A6: dom (S . A) = H₁(A) by A3;
then reconsider x = o as Surreal by A4;
set Nx = ||.x.||;
set xx = (L_ ||.x.||) \/ (R_ ||.x.||);
set xxZ = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No};
A7: ( x in Day A & 0_No < x ) by A6, A4, Def10;
A8: born x c= A by SURREAL0:def 18, A6, A4;
then A9: Positives (born x) c= Positives A by Th23;
A10: x is positive by A6, A4, Def10;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x) by A7, Def8, Th24;
then A11: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives A by A9, XBOOLE_1:1;
A12: dom (S . A) c= dom (union (rng S)) by A5, SURREALR:2;
A13: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= dom (union (rng (S | A)))

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
set b = born o;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A10, Th20;
then A15: born o in born x by SURREALO:1, A14;
born o in dom S by A5, A8, A15, ORDINAL1:10;
then A16: born o in dom (S | A) by A15, A8, RELAT_1:57;
then A17: dom ((S | A) . (born o)) c= dom (union (rng (S | A))) by SURREALR:2;
A18: (S | A) . (born o) = S . (born o) by A16, FUNCT_1:47;
A19: o is positive by A10, Th21, A14;
A20: dom (S . (born o)) = H₁( born o) by A3, A15, A8, A5, ORDINAL1:10;
o in Day (born o) by SURREAL0:def 18;
then o in H₁( born o) by Def10, A19;
hence o in dom (union (rng (S | A))) by A18, A17, A20; :: thesis:

end;

A21: ( dom ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} = dom ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) ) by A12, A6, A11, XBOOLE_1:1, A13, RELAT_1:62;
for a being object st a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} holds
((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a

let a be object ; :: thesis:
assume A22: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider a = a as Surreal by SURREAL0:def 16;
set b = born a;
A23: ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (union (rng (S | A))) . a by A22, FUNCT_1:49;
A24: ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (union (rng S)) . a by A22, FUNCT_1:49;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A10, Th20;
then A25: born a in born x by SURREALO:1, A22;
A26: a is positive by A10, Th21, A22;
A27: dom (S . (born a)) = H₁( born a) by A3, A8, A25, A5, ORDINAL1:10;
a in Day (born a) by SURREAL0:def 18;
then ( a in dom (S . (born a)) & born a in A ) by Def10, A26, A27, A25, A8;
hence ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a by A23, A24, SURREALR:5; :: thesis:

end;

then (union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) = (union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) by A21, FUNCT_1:2;
then ( divL (||.x.||,(union (rng (S | A)))) = divL (||.x.||,(union (rng S))) & divR (||.x.||,(union (rng (S | A)))) = divR (||.x.||,(union (rng S))) ) by Th17;
hence H₂(o,S | A) = H₂(o,S) ; :: thesis:

end;

consider S being c=-monotone Function-yielding Sequence such that
A28: dom S = succ A and
A29: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S | B) ) ) from SURREALR:sch 1(A2, A1);
consider SA being ManySortedSet of H₁(A) such that
A30: ( S . A = SA & ( for o being object st o in H₁(A) holds
SA . o = H₂(o,S | A) ) ) by A29, ORDINAL1:6;
take SA ; :: thesis:
take S ; :: thesis:
thus ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) ) by A28, A29, A30; :: thesis:

end;

let dA1, dA2 be ManySortedSet of Positives A; :: thesis:
deffunc H₁( Ordinal) -> Subset of (Day $1) = Positives $1;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (divL (||.$1.||,(union (rng $2))))),(Union (divR (||.$1.||,(union (rng $2)))))];
given S1 being c=-monotone Function-yielding Sequence such that A31: ( dom S1 = succ A & dA1 = S1 . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S1 . B = SB & ( for x being object st x in Positives B holds
SB . x = H₂(x,S1 | B) ) ) ) ) ; :: thesis:
given S2 being c=-monotone Function-yielding Sequence such that A32: ( dom S2 = succ A & dA2 = S2 . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S2 . B = SB & ( for x being object st x in Positives B holds
SB . x = H₂(x,S2 | B) ) ) ) ) ; :: thesis:
A33: ( succ A c= dom S1 & succ A c= dom S2 ) by A31, A32;
A34: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S1 | B) ) ) by A31;
A35: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S2 | B) ) ) by A32;
S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A33, A34, A35);
then S1 | (succ A) = S2 by A32;
hence dA1 = dA2 by A31, A32; :: thesis:

end;

:: deftheorem Def11 defines No_inverse_op SURREALI:def 11 :

theorem Th25: :: SURREALI:25

for S being c=-monotone Function-yielding Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for o being object st o in Positives B holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | B)))))),(Union (divR (||.o.||,(union (rng (S | B))))))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_inverse_op A = S . A

deffunc H₁( Ordinal) -> Subset of (Day $1) = Positives $1;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (divL (||.$1.||,(union (rng $2))))),(Union (divR (||.$1.||,(union (rng $2)))))];
let S1 be c=-monotone Function-yielding Sequence; :: thesis:
assume A1: for B being Ordinal st B in dom S1 holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S1 | B) ) ) ; :: thesis:
let A be Ordinal; :: thesis:
assume A2: A in dom S1 ; :: thesis:
A3: succ A c= dom S1 by A2, ORDINAL1:21;
consider S2 being c=-monotone Function-yielding Sequence such that
A4: ( dom S2 = succ A & S2 . A = No_inverse_op A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S2 | B) ) ) ) ) by Def11;
A5: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S1 | B) ) ) by A1, A3;
A6: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S2 | B) ) ) by A4;
A7: ( succ A c= dom S1 & succ A c= dom S2 ) by A2, ORDINAL1:21, A4;
A8: S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A7, A5, A6);
A in succ A by ORDINAL1:8;
hence No_inverse_op A = S1 . A by A4, A8, FUNCT_1:49; :: thesis:

end;

definition

let x be Surreal;

func inv x -> object equals :: SURREALI:def 12
(No_inverse_op (born x)) . x;

coherence ;

end;

:: deftheorem defines inv SURREALI:def 12 :

definition

let x be Surreal;

func No_inverses_on x -> Function means :Def13: :: SURREALI:def 13
( dom it = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
it . y = inv y ) );

defpred S₁[ object , object ] means for y being Surreal st y = $1 holds
$2 = inv y;
A1: for e being object st e in ((L_ x) \/ (R_ x)) \ {0_No} holds
ex u being object st S₁[e,u]

let e be object ; :: thesis:
assume A2: e in ((L_ x) \/ (R_ x)) \ {0_No} ; :: thesis:
reconsider e = e as Surreal by A2, SURREAL0:def 16;
take inv e ; :: thesis:
thus S₁[e, inv e] ; :: thesis:

end;

consider f being Function such that
A3: dom f = ((L_ x) \/ (R_ x)) \ {0_No} and
A4: for e being object st e in ((L_ x) \/ (R_ x)) \ {0_No} holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
take f ; :: thesis:
thus dom f = ((L_ x) \/ (R_ x)) \ {0_No} by A3; :: thesis:
let y be Surreal; :: thesis:
thus ( y in ((L_ x) \/ (R_ x)) \ {0_No} implies f . y = inv y ) by A4; :: thesis:

end;

let i1, i2 be Function; :: thesis:
assume that
A5: dom i1 = ((L_ x) \/ (R_ x)) \ {0_No} and
A6: for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
i1 . y = inv y and
A7: dom i2 = ((L_ x) \/ (R_ x)) \ {0_No} and
A8: for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
i2 . y = inv y ; :: thesis:
for o being object st o in ((L_ x) \/ (R_ x)) \ {0_No} holds
i1 . o = i2 . o

let o be object ; :: thesis:
assume A9: o in ((L_ x) \/ (R_ x)) \ {0_No} ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
i1 . o = inv o by A9, A6;
hence i1 . o = i2 . o by A9, A8; :: thesis:

end;

hence i1 = i2 by A5, A7, FUNCT_1:2; :: thesis:

end;

:: deftheorem Def13 defines No_inverses_on SURREALI:def 13 :

theorem Th26: :: SURREALI:26

for x being Surreal
for Inv being Function st x is positive & No_inverses_on ||.x.|| c= Inv holds
inv x = [(Union (divL (||.x.||,Inv))),(Union (divR (||.x.||,Inv)))]

let x be Surreal; :: thesis:
let Inv be Function; :: thesis:
set A = born x;
set Nx = ||.x.||;
assume A1: ( x is positive & No_inverses_on ||.x.|| c= Inv ) ; :: thesis:
consider S being c=-monotone Function-yielding Sequence such that
A2: ( dom S = succ (born x) & No_inverse_op (born x) = S . (born x) ) and
A3: for B being Ordinal st B in succ (born x) holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for o being object st o in Positives B holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | B)))))),(Union (divR (||.o.||,(union (rng (S | B))))))] ) ) by Def11;
consider SB being ManySortedSet of Positives (born x) such that
A4: S . (born x) = SB and
A5: for o being object st o in Positives (born x) holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | (born x))))))),(Union (divR (||.o.||,(union (rng (S | (born x)))))))] by A3, ORDINAL1:6;
set UA = union (rng (S | (born x)));
x in Day (born x) by SURREAL0:def 18;
then A6: x in Positives (born x) by A1, Def10;
set XX = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No};
A7: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x) by A1, Th24;
A8: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A1, Th20;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= dom (union (rng (S | (born x))))

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
set b = born o;
A10: 0_No < o by A7, A9, Def10;
o in Day (born o) by SURREAL0:def 18;
then A11: o in Positives (born o) by A10, Def10;
A12: born o in born x by A9, A8, SURREALO:1;
born o in succ (born x) by ORDINAL1:8, A9, A8, SURREALO:1;
then ex SB being ManySortedSet of Positives (born o) st
( S . (born o) = SB & ( for o being object st o in Positives (born o) holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | (born o))))))),(Union (divR (||.o.||,(union (rng (S | (born o)))))))] ) ) by A3;
then o in dom (S . (born o)) by A11, PARTFUN1:def 2;
hence o in dom (union (rng (S | (born x)))) by A12, SURREALR:5; :: thesis:

end;

let a be object ; :: thesis:
assume A15: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider o = a as Surreal by SURREAL0:def 16;
A16: ((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (union (rng (S | (born x)))) . a by A15, FUNCT_1:49;
set b = born o;
A17: 0_No < o by A7, A15, Def10;
o in Day (born o) by SURREAL0:def 18;
then A18: o in Positives (born o) by A17, Def10;
A19: born o in born x by A15, A8, SURREALO:1;
A20: born o in succ (born x) by ORDINAL1:8, A15, A8, SURREALO:1;
then ex SB being ManySortedSet of Positives (born o) st
( S . (born o) = SB & ( for o being object st o in Positives (born o) holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | (born o))))))),(Union (divR (||.o.||,(union (rng (S | (born o)))))))] ) ) by A3;
then A21: o in dom (S . (born o)) by A18, PARTFUN1:def 2;
then A22: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A19, SURREALR:5;
A23: born o in dom S by ORDINAL1:8, A15, A8, SURREALO:1, A2;
A24: No_inverse_op (born o) = S . (born o) by A2, A3, Th25, A20;
A25: (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . o = Inv . o by A15, FUNCT_1:49;
A26: o in dom (No_inverses_on ||.x.||) by A15, Def13;
(No_inverses_on ||.x.||) . o = inv o by A15, Def13;
then [o,(inv o)] in No_inverses_on ||.x.|| by A26, FUNCT_1:1;
then (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . o = inv o by A1, A25, FUNCT_1:1;
hence ((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a by A24, A16, A22, A21, A23, SURREALR:2; :: thesis:

end;

then (union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) = Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) by A13, A14, FUNCT_1:2;
then ( divL (||.x.||,(union (rng (S | (born x))))) = divL (||.x.||,Inv) & divR (||.x.||,(union (rng (S | (born x))))) = divR (||.x.||,Inv) ) by Th17;
hence inv x = [(Union (divL (||.x.||,Inv))),(Union (divR (||.x.||,Inv)))] by A6, A4, A5, A2; :: thesis:

end;

theorem Th27: :: SURREALI:27

for y being Surreal
for f being Function st dom f = NAT & y in Union f holds
ex n being Nat st
( y in f . n & ( for m being Nat st y in f . m holds
n <= m ) )

let y be Surreal; :: thesis:
let f be Function; :: thesis:
assume A1: ( dom f = NAT & y in Union f ) ; :: thesis:
defpred S₁[ Nat] means y in f . $1;
consider n being object such that
A2: ( n in dom f & y in f . n ) by A1, CARD_5:2;
reconsider n = n as Nat by A1, A2;
y in f . n by A2;
then A3: ex n being Nat st S₁[n] ;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
hence ex n being Nat st
( y in f . n & ( for m being Nat st y in f . m holds
n <= m ) ) ; :: thesis:

end;

theorem Th28: :: SURREALI:28

for x, y, x1, x1R, y1, y1R being Surreal st 0_No < x1 & x1 * x1R == 1_No & 0_No < y1 & y1 * y1R == 1_No & x * y1 < y * x1 holds
x * x1R < y * y1R

let x, y be Surreal; :: thesis:
let x1, x1R, y1, y1R be Surreal; :: thesis:
assume A1: ( 0_No < x1 & x1 * x1R == 1_No & 0_No < y1 & y1 * y1R == 1_No & x * y1 < y * x1 ) ; :: thesis:
A2: ( 0_No <= x1 & 0_No <= y1 ) by A1;
1_No is positive ;
then ( 0_No < x1 * x1R & 0_No < y1 * y1R ) by A1, SURREALO:4;
then A3: ( 0_No < x1R & 0_No < y1R ) by A2, SURREALR:72;
then (x * y1) * y1R < (y * x1) * y1R by A1, SURREALR:70;
then A4: ((x * y1) * y1R) * x1R < ((y * x1) * y1R) * x1R by A3, SURREALR:70;
( (x * y1) * y1R == x * (y1 * y1R) & x * (y1 * y1R) == x * 1_No & x * 1_No = x ) by SURREALR:51, SURREALR:69, A1;
then (x * y1) * y1R == x by SURREALO:4;
then A5: ((x * y1) * y1R) * x1R == x * x1R by SURREALR:51;
( ((y * x1) * y1R) * x1R == (y * (x1 * y1R)) * x1R & (y * (x1 * y1R)) * x1R == y * ((x1 * y1R) * x1R) ) by SURREALR:51, SURREALR:69;
then ( ((y * x1) * y1R) * x1R == y * ((x1 * y1R) * x1R) & y * ((x1 * y1R) * x1R) == y * (y1R * (x1 * x1R)) ) by SURREALR:69, SURREALO:4, SURREALR:51;
then A6: ((y * x1) * y1R) * x1R == y * (y1R * (x1 * x1R)) by SURREALO:4;
( y1R * (x1 * x1R) == y1R * 1_No & y1R * 1_No = y1R ) by SURREALR:51, A1;
then y * (y1R * (x1 * x1R)) == y * y1R by SURREALR:51;
then ((y * x1) * y1R) * x1R == y * y1R by A6, SURREALO:4;
then ((x * y1) * y1R) * x1R < y * y1R by A4, SURREALO:4;
hence x * x1R < y * y1R by A5, SURREALO:4; :: thesis:

end;

theorem Th29: :: SURREALI:29

for x, x1, x2, y1, y2 being Surreal holds
( ((1_No + ((x2 - x) * y2)) * x1) + (- ((1_No + ((x1 - x) * y1)) * x2)) == ((x1 - x2) * (1_No - (x * y1))) + (((y1 - y2) * x1) * (x - x2)) & ((1_No + ((x2 - x) * y2)) * x1) - ((1_No + ((x1 - x) * y1)) * x2) == ((x1 - x2) * (1_No - (x * y2))) + (((y2 - y1) * x2) * (x1 - x)) )

let x, x1, x2, y1, y2 be Surreal; :: thesis:
( ((x2 + (- x)) * y2) * x1 == ((x2 * y2) + ((- x) * y2)) * x1 & ((x2 * y2) + ((- x) * y2)) * x1 == ((x2 * y2) * x1) + (((- x) * y2) * x1) ) by SURREALR:51, SURREALR:67;
then ((x2 + (- x)) * y2) * x1 == ((x2 * y2) * x1) + (((- x) * y2) * x1) by SURREALO:4;
then ( (1_No + ((x2 + (- x)) * y2)) * x1 == (1_No * x1) + (((x2 + (- x)) * y2) * x1) & (1_No * x1) + (((x2 + (- x)) * y2) * x1) == x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1)) ) by SURREALR:43, SURREALR:67;
then A1: (1_No + ((x2 + (- x)) * y2)) * x1 == x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1)) by SURREALO:4;
( ((x1 + (- x)) * y1) * x2 == ((x1 * y1) + ((- x) * y1)) * x2 & ((x1 * y1) + ((- x) * y1)) * x2 == ((x1 * y1) * x2) + (((- x) * y1) * x2) ) by SURREALR:51, SURREALR:67;
then ((x1 + (- x)) * y1) * x2 == ((x1 * y1) * x2) + (((- x) * y1) * x2) by SURREALO:4;
then ( (1_No + ((x1 + (- x)) * y1)) * x2 == (1_No * x2) + (((x1 + (- x)) * y1) * x2) & (1_No * x2) + (((x1 + (- x)) * y1) * x2) == x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2)) ) by SURREALR:43, SURREALR:67;
then (1_No + ((x1 + (- x)) * y1)) * x2 == x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2)) by SURREALO:4;
then A2: - ((1_No + ((x1 + (- x)) * y1)) * x2) == - (x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2))) by SURREALR:10;
A3: (x1 + (- x2)) * 1_No = x1 + (- x2) ;
(x1 + (- x2)) * (- (x * y1)) == (x1 * (- (x * y1))) + ((- x2) * (- (x * y1))) by SURREALR:67;
then ( (x1 + (- x2)) * (1_No + (- (x * y1))) == (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y1))) & (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y1))) == (x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) ) by A3, SURREALR:43, SURREALR:67;
then A4: (x1 + (- x2)) * (1_No + (- (x * y1))) == (x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) by SURREALO:4;
set X3 = x1 * (- (x * y1));
set X4 = (- x2) * (- (x * y1));
set Y3 = (y1 * x1) * x;
set X5 = ((- y2) * x1) * x;
set X6 = (y1 * x1) * (- x2);
set X7 = ((- y2) * x1) * (- x2);
A5: ( ((y1 * x1) + ((- y2) * x1)) * x == ((y1 * x1) * x) + (((- y2) * x1) * x) & ((y1 * x1) + ((- y2) * x1)) * (- x2) == ((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)) ) by SURREALR:67;
( ((y1 + (- y2)) * x1) * (x + (- x2)) == ((y1 * x1) + ((- y2) * x1)) * (x + (- x2)) & ((y1 * x1) + ((- y2) * x1)) * (x + (- x2)) == (((y1 * x1) + ((- y2) * x1)) * x) + (((y1 * x1) + ((- y2) * x1)) * (- x2)) ) by SURREALR:51, SURREALR:67;
then ( ((y1 + (- y2)) * x1) * (x + (- x2)) == (((y1 * x1) + ((- y2) * x1)) * x) + (((y1 * x1) + ((- y2) * x1)) * (- x2)) & (((y1 * x1) + ((- y2) * x1)) * x) + (((y1 * x1) + ((- y2) * x1)) * (- x2)) == (((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))) ) by A5, SURREALO:4, SURREALR:43;
then ((y1 + (- y2)) * x1) * (x + (- x2)) == (((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))) by SURREALO:4;
then A6: ((x1 + (- x2)) * (1_No + (- (x * y1)))) + (((y1 + (- y2)) * x1) * (x + (- x2))) == ((x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1))))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)))) by A4, SURREALR:43;
A7: ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)))) = ((- x2) * (- (x * y1))) + ((x1 * (- (x * y1))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))))) by SURREALR:37
.= (((x1 * (- (x * y1))) + (((y1 * x1) * x) + (((- y2) * x1) * x))) + ((((- y2) * x1) * (- x2)) + ((y1 * x1) * (- x2)))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + (((- y2) * x1) * x)) + ((((- y2) * x1) * (- x2)) + ((y1 * x1) * (- x2)))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= (((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + (((- y2) * x1) * x)) + (((- y2) * x1) * (- x2))) + ((y1 * x1) * (- x2))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + ((y1 * x1) * (- x2))) + ((- x2) * (- (x * y1))) by SURREALR:37
.= (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) by SURREALR:37 ;
A8: ((x1 + (- x2)) + ((x1 * (- (x * y1))) + ((- x2) * (- (x * y1))))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2)))) = (x1 + (- x2)) + (((x1 * (- (x * y1))) + ((- x2) * (- (x * y1)))) + ((((y1 * x1) * x) + (((- y2) * x1) * x)) + (((y1 * x1) * (- x2)) + (((- y2) * x1) * (- x2))))) by SURREALR:37
.= ((x1 + (- x2)) + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) by A7, SURREALR:37
.= (x1 + ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + (- x2))) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) by SURREALR:37
.= x1 + (((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + (- x2)) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by SURREALR:37
.= x1 + ((((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))))) by SURREALR:37
.= (x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by SURREALR:37 ;
A9: - (x1 * (x * y1)) == - ((y1 * x1) * x) by SURREALR:65, SURREALR:69;
x1 * (- (x * y1)) == - ((y1 * x1) * x) by A9, SURREALR:58;
then ( (x1 * (- (x * y1))) + ((y1 * x1) * x) == (- ((y1 * x1) * x)) + ((y1 * x1) * x) & (- ((y1 * x1) * x)) + ((y1 * x1) * x) = ((y1 * x1) * x) - ((y1 * x1) * x) & ((y1 * x1) * x) - ((y1 * x1) * x) == 0_No ) by SURREALR:39, SURREALR:43;
then A10: (x1 * (- (x * y1))) + ((y1 * x1) * x) == 0_No by SURREALO:4;
((- y2) * x1) * x = (- (y2 * x1)) * x by SURREALR:58
.= - ((y2 * x1) * x) by SURREALR:58
.= (y2 * x1) * (- x) by SURREALR:58 ;
then A11: ((- y2) * x1) * x == ((- x) * y2) * x1 by SURREALR:69;
((- y2) * x1) * (- x2) = (- (y2 * x1)) * (- x2) by SURREALR:58
.= - (- ((y2 * x1) * x2)) by SURREALR:58
.= x2 * (y2 * x1) ;
then ((- y2) * x1) * (- x2) == (x2 * y2) * x1 by SURREALR:69;
then (((- y2) * x1) * x) + (((- y2) * x1) * (- x2)) == ((x2 * y2) * x1) + (((- x) * y2) * x1) by A11, SURREALR:43;
then A12: ( ((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))) == 0_No + (((x2 * y2) * x1) + (((- x) * y2) * x1)) & 0_No + (((x2 * y2) * x1) + (((- x) * y2) * x1)) = ((x2 * y2) * x1) + (((- x) * y2) * x1) ) by A10, SURREALR:43;
(- x2) * (- (x * y1)) = ((- x) * y1) * (- x2) by SURREALR:58
.= - (((- x) * y1) * x2) by SURREALR:58 ;
then A13: (- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1)))) == (- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2))) by SURREALR:58;
x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1)) == x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2)))) by A12, SURREALR:43;
then A14: (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + ((- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)))) == (x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by A13, SURREALR:43;
- (x2 + (((x1 * y1) * x2) + (((- x) * y1) * x2))) = (- x2) + (- (((x1 * y1) * x2) + (((- x) * y1) * x2))) by SURREALR:40
.= (- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2))) by SURREALR:40 ;
then A15: (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + ((- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)))) == ((1_No + ((x2 + (- x)) * y2)) * x1) + (- ((1_No + ((x1 + (- x)) * y1)) * x2)) by A1, A2, SURREALR:43;
then ((1_No + ((x2 + (- x)) * y2)) * x1) + (- ((1_No + ((x1 + (- x)) * y1)) * x2)) == (x1 + (((x1 * (- (x * y1))) + ((y1 * x1) * x)) + ((((- y2) * x1) * x) + (((- y2) * x1) * (- x2))))) + ((- x2) + (((y1 * x1) * (- x2)) + ((- x2) * (- (x * y1))))) by A14, SURREALO:4;
hence ((1_No + ((x2 - x) * y2)) * x1) + (- ((1_No + ((x1 - x) * y1)) * x2)) == ((x1 - x2) * (1_No - (x * y1))) + (((y1 - y2) * x1) * (x - x2)) by A6, A8, SURREALO:4; :: thesis:
A16: (x1 + (- x2)) * 1_No = x1 + (- x2) ;
(x1 + (- x2)) * (- (x * y2)) == (x1 * (- (x * y2))) + ((- x2) * (- (x * y2))) by SURREALR:67;
then ( (x1 + (- x2)) * (1_No + (- (x * y2))) == (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y2))) & (x1 + (- x2)) + ((x1 + (- x2)) * (- (x * y2))) == (x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) ) by A16, SURREALR:43, SURREALR:67;
then A17: (x1 + (- x2)) * (1_No + (- (x * y2))) == (x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) by SURREALO:4;
A18: ( ((y2 * x2) + ((- y1) * x2)) * x1 == ((y2 * x2) * x1) + (((- y1) * x2) * x1) & ((y2 * x2) + ((- y1) * x2)) * (- x) == ((y2 * x2) * (- x)) + (((- y1) * x2) * (- x)) ) by SURREALR:67;
( ((y2 + (- y1)) * x2) * (x1 + (- x)) == ((y2 * x2) + ((- y1) * x2)) * (x1 + (- x)) & ((y2 * x2) + ((- y1) * x2)) * (x1 + (- x)) == (((y2 * x2) + ((- y1) * x2)) * x1) + (((y2 * x2) + ((- y1) * x2)) * (- x)) ) by SURREALR:51, SURREALR:67;
then ( ((y2 + (- y1)) * x2) * (x1 + (- x)) == (((y2 * x2) + ((- y1) * x2)) * x1) + (((y2 * x2) + ((- y1) * x2)) * (- x)) & (((y2 * x2) + ((- y1) * x2)) * x1) + (((y2 * x2) + ((- y1) * x2)) * (- x)) == (((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x))) ) by A18, SURREALO:4, SURREALR:43;
then A19: ((y2 + (- y1)) * x2) * (x1 + (- x)) == (((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x))) by SURREALO:4;
set A2 = (y2 * x2) * x1;
set A3 = x1 * (- (x * y2));
set A4 = - x2;
set A5 = ((- y1) * x2) * x1;
set A6 = ((- y1) * x2) * (- x);
set A7 = (- x2) * (- (x * y2));
set B7 = (y2 * x2) * (- x);
A20: ((x1 + (- x2)) * (1_No + (- (x * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- x))) == ((x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2))))) + ((((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x)))) by A19, A17, SURREALR:43;
(((- x2) * (- (x * y2))) + (x1 * (- (x * y2)))) + (((y2 * x2) * (- x)) + ((y2 * x2) * x1)) = (((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) + ((y2 * x2) * (- x))) + ((y2 * x2) * x1) by SURREALR:37
.= ((x1 * (- (x * y2))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((y2 * x2) * x1) by SURREALR:37
.= (((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x))) by SURREALR:37 ;
then ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) = ((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) by SURREALR:37;
then A21: (x1 + (- x2)) + (((x1 * (- (x * y2))) + ((- x2) * (- (x * y2)))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))))) = x1 + ((((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) + (- x2)) by SURREALR:37
.= x1 + (((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + (((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) + (- x2))) by SURREALR:37
.= (x1 + ((((y2 * x2) * x1) + (x1 * (- (x * y2)))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x))))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) by SURREALR:37
.= ((x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) by SURREALR:37 ;
A22: (((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((y2 * x2) * (- x)) + (((- y1) * x2) * (- x))) = ((((y2 * x2) * x1) + (((- y1) * x2) * x1)) + (((- y1) * x2) * (- x))) + ((y2 * x2) * (- x)) by SURREALR:37
.= (((y2 * x2) * x1) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) + ((y2 * x2) * (- x)) by SURREALR:37
.= (((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) by SURREALR:37 ;
A23: ((x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2))))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) = ((x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) by A21, SURREALR:37;
A24: ((y2 * x2) * x1) + (x1 * (- (x * y2))) = ((x2 * y2) * x1) + (((- x) * y2) * x1) by SURREALR:58;
((- y1) * x2) * x1 = (- (y1 * x2)) * x1 by SURREALR:58
.= - ((y1 * x2) * x1) by SURREALR:58 ;
then A25: ((- y1) * x2) * x1 == - ((x1 * y1) * x2) by SURREALR:65, SURREALR:69;
A26: ((- y1) * x2) * (- x) = (- (y1 * x2)) * (- x) by SURREALR:58
.= - ((y1 * x2) * (- x)) by SURREALR:58 ;
((- y1) * x2) * (- x) == - (((- x) * y1) * x2) by A26, SURREALR:65, SURREALR:69;
then (((- y1) * x2) * x1) + (((- y1) * x2) * (- x)) == (- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)) by A25, SURREALR:43;
then A27: (- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x))) == (- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2))) by SURREALR:43;
A28: (- x2) * (- (x * y2)) = - (x2 * (- (x * y2))) by SURREALR:58;
- (x * y2) = (- x) * y2 by SURREALR:58;
then x2 * (- (x * y2)) == (y2 * x2) * (- x) by SURREALR:69;
then (- x2) * (- (x * y2)) == - ((y2 * x2) * (- x)) by A28, SURREALR:10;
then ( ((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)) == (- ((y2 * x2) * (- x))) + ((y2 * x2) * (- x)) & (- ((y2 * x2) * (- x))) + ((y2 * x2) * (- x)) = ((y2 * x2) * (- x)) - ((y2 * x2) * (- x)) & ((y2 * x2) * (- x)) - ((y2 * x2) * (- x)) == 0_No ) by SURREALR:39, SURREALR:43;
then A29: ((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)) == 0_No by SURREALO:4;
(x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x))) == (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + 0_No by A29, SURREALR:43, A24;
then ((x1 + (((y2 * x2) * x1) + (x1 * (- (x * y2))))) + (((- x2) * (- (x * y2))) + ((y2 * x2) * (- x)))) + ((- x2) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) == (x1 + (((x2 * y2) * x1) + (((- x) * y2) * x1))) + ((- x2) + ((- ((x1 * y1) * x2)) + (- (((- x) * y1) * x2)))) by A27, SURREALR:43;
then ((x1 + (- x2)) + ((x1 * (- (x * y2))) + ((- x2) * (- (x * y2))))) + ((((y2 * x2) * x1) + ((y2 * x2) * (- x))) + ((((- y1) * x2) * x1) + (((- y1) * x2) * (- x)))) == ((1_No + ((x2 + (- x)) * y2)) * x1) + (- ((1_No + ((x1 + (- x)) * y1)) * x2)) by A23, SURREALO:4, A15;
hence ((1_No + ((x2 - x) * y2)) * x1) - ((1_No + ((x1 - x) * y1)) * x2) == ((x1 - x2) * (1_No - (x * y2))) + (((y2 - y1) * x2) * (x1 - x)) by A22, A20, SURREALO:4; :: thesis:

end;

theorem Th30: :: SURREALI:30

for x, y, x1, y1, Ix1 being Surreal st x1 * Ix1 == 1_No holds
((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1)))

let x, y be Surreal; :: thesis:
let x1, y1, Ix1 be Surreal; :: thesis:
assume A1: x1 * Ix1 == 1_No ; :: thesis:
( x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1) == (1_No + ((x1 + (- x)) * y1)) * (x1 * Ix1) & (1_No + ((x1 + (- x)) * y1)) * (x1 * Ix1) == (1_No + ((x1 + (- x)) * y1)) * 1_No & (1_No + ((x1 + (- x)) * y1)) * 1_No = 1_No + ((x1 + (- x)) * y1) ) by A1, SURREALR:69, SURREALR:51;
then x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1) == 1_No + ((x1 + (- x)) * y1) by SURREALO:4;
then A2: ( - (x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1)) == - (1_No + ((x1 + (- x)) * y1)) & - (1_No + ((x1 + (- x)) * y1)) = (- 1_No) + (- ((x1 + (- x)) * y1)) ) by SURREALR:10, SURREALR:40;
- ((x1 + (- x)) * y1) == - ((x1 * y1) + ((- x) * y1)) by SURREALR:65, SURREALR:67;
then (- 1_No) + (- ((x1 + (- x)) * y1)) == (- 1_No) + (- ((x1 * y1) + ((- x) * y1))) by SURREALR:43;
then A3: - (x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1)) == (- 1_No) + (- ((x1 * y1) + ((- x) * y1))) by A2, SURREALO:4;
A4: x1 * (- ((1_No + ((x1 + (- x)) * y1)) * Ix1)) == (- 1_No) + (- ((x1 * y1) + ((- x) * y1))) by A3, SURREALR:58;
( x1 * (y + (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) == (x1 * y) + (x1 * (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) & (x1 * y) + (x1 * (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) == (x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1)))) ) by A4, SURREALR:43, SURREALR:67;
then x1 * (y + (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) == (x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1)))) by SURREALO:4;
then A5: 1_No + (x1 * (y + (- ((1_No + ((x1 + (- x)) * y1)) * Ix1)))) == 1_No + ((x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1))))) by SURREALR:43;
A6: 1_No - 1_No == 0_No by SURREALR:39;
- ((- x) * y1) = - (- (x * y1)) by SURREALR:58
.= x * y1 ;
then A7: (x1 * y) + (- ((x1 * y1) + ((- x) * y1))) = (x1 * y) + ((- (x1 * y1)) + (x * y1)) by SURREALR:40
.= ((x1 * y) + (x * y1)) + (- (x1 * y1)) by SURREALR:37 ;
1_No + ((x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1))))) = 1_No + ((- 1_No) + ((x1 * y) + (- ((x1 * y1) + ((- x) * y1))))) by SURREALR:37
.= (1_No + (- 1_No)) + ((x1 * y) + (- ((x1 * y1) + ((- x) * y1)))) by SURREALR:37 ;
then ( 1_No + ((x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1))))) == 0_No + (((x1 * y) + (x * y1)) + (- (x1 * y1))) & 0_No + (((x1 * y) + (x * y1)) + (- (x1 * y1))) = ((x1 * y) + (x * y1)) + (- (x1 * y1)) ) by A7, A6, SURREALR:43;
hence ((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1))) by A5, SURREALO:4; :: thesis:

end;

defpred S₁[ Ordinal] means for x being Surreal st born x = $1 & x is positive holds
( inv x is surreal & ( for y being Surreal st y = inv x holds
x * y == 1_No ) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let x be Surreal; :: thesis:
assume A3: ( born x = D & x is positive ) ; :: thesis:
set Nx = ||.x.||;
set Inv = No_inverses_on ||.x.||;
A4: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A3, Th20;
A5: No_inverses_on ||.x.|| is ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} -surreal-valued

let o be object ; :: according to SURREALI:def 7 :: thesis:
assume A6: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( born o in born x & o is positive ) by A6, A4, A3, SURREALO:1, Th21;
then inv o is surreal by A2, A3;
hence (No_inverses_on ||.x.||) . o is Surreal by A6, Def13; :: thesis:

end;

then A7: ( Union (divL (||.x.||,(No_inverses_on ||.x.||))) is surreal-membered & Union (divR (||.x.||,(No_inverses_on ||.x.||))) is surreal-membered ) by Th10;
defpred S₂[ Nat] means ( ( for yL being Surreal st yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . $1 holds
||.x.|| * yL < 1_No ) & ( for yR being Surreal st yR in (divR (||.x.||,(No_inverses_on ||.x.||))) . $1 holds
1_No < ||.x.|| * yR ) );
A8: S₂[ 0 ]

thus for yL being Surreal st yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . 0 holds
||.x.|| * yL < 1_No :: thesis:

A9: 1_No is positive ;
let yL be Surreal; :: thesis:
assume A10: yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . 0 ; :: thesis:
(divL (||.x.||,(No_inverses_on ||.x.||))) . 0 = {0_No} by Th1;
then yL = 0_No by A10, TARSKI:def 1;
hence ||.x.|| * yL < 1_No by A9; :: thesis:

end;

thus for yR being Surreal st yR in (divR (||.x.||,(No_inverses_on ||.x.||))) . 0 holds
1_No < ||.x.|| * yR by Th1; :: thesis:

end;

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

let n be Nat; :: thesis:
assume A12: S₂[n] ; :: thesis:
set n1 = n + 1;
A13: ( (divL (||.x.||,(No_inverses_on ||.x.||))) . n c= Union (divL (||.x.||,(No_inverses_on ||.x.||))) & (divR (||.x.||,(No_inverses_on ||.x.||))) . n c= Union (divR (||.x.||,(No_inverses_on ||.x.||))) ) by ABCMIZ_1:1;
thus for yL being Surreal st yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . (n + 1) holds
||.x.|| * yL < 1_No :: thesis:

suppose yL in (divL (||.x.||,(No_inverses_on ||.x.||))) . n ; :: thesis:

hence ||.x.|| * yL < 1_No by A12; :: thesis:

end;

suppose yL in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider yL1 being object such that
A15: ( yL1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . n & yL in divs (yL1,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider yL1 = yL1 as Surreal by A7, A15, A13;
consider xR being object such that
A16: ( xR in R_ ||.x.|| & xR <> 0_No ) and
A17: yL = (1_No +' ((xR +' (-' ||.x.||)) *' yL1)) *' ((No_inverses_on ||.x.||) . xR) by A15, Def2;
reconsider xR = xR as Surreal by A16, SURREAL0:def 16;
A18: xR in (L_ ||.x.||) \/ (R_ ||.x.||) by A16, XBOOLE_0:def 3;
then A19: ( born xR in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A20: xR is positive by A3, A16, Def9;
then reconsider IxR = inv xR as Surreal by A3, A2, A19;
A21: xR * IxR == 1_No by A3, A2, A19, A20;
( ||.x.|| in {||.x.||} & {||.x.||} << R_ ||.x.|| ) by SURREALO:11, TARSKI:def 1;
then A22: ||.x.|| + (- ||.x.||) < xR + (- ||.x.||) by A16, SURREALR:32;
||.x.|| - ||.x.|| == 0_No by SURREALR:39;
then A23: 0_No < xR + (- ||.x.||) by A22, SURREALO:4;
A24: ( (||.x.|| * yL1) * (xR + (- ||.x.||)) < 1_No * (xR + (- ||.x.||)) & 1_No * (xR + (- ||.x.||)) = xR + (- ||.x.||) ) by A12, A15, A23, SURREALR:70;
xR in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A18, A16, ZFMISC_1:56;
then A25: ||.x.|| * yL = ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) by A17, Def13;
A26: ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) == ||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:51, SURREALR:67;
||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:67;
then A27: ||.x.|| * yL == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by A26, A25, SURREALO:4;
A28: 0_No < xR * IxR by SURREALO:4, Def8, A21;
0_No <= xR by A20;
then 0_No < IxR by A28, SURREALR:72;
then A29: ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR < (xR + (- ||.x.||)) * IxR by A24, SURREALR:70;
A30: ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by SURREALR:51, SURREALR:69;
( ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) & (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) ) by SURREALR:69;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) by SURREALO:4;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by A30, SURREALO:4;
then ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) < (xR + (- ||.x.||)) * IxR by A29, SURREALO:4;
then (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) < (||.x.|| * (1_No * IxR)) + ((xR + (- ||.x.||)) * IxR) by SURREALR:44;
then A31: ||.x.|| * yL < (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) by A27, SURREALO:4;
(- ||.x.||) * IxR = - (||.x.|| * IxR) by SURREALR:58;
then (xR + (- ||.x.||)) * IxR == (xR * IxR) + (- (||.x.|| * IxR)) by SURREALR:67;
then A32: (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) by SURREALR:43;
A33: (||.x.|| * IxR) - (||.x.|| * IxR) == 0_No by SURREALR:39;
(||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) = ((||.x.|| * IxR) + (- (||.x.|| * IxR))) + (xR * IxR) by SURREALR:37;
then (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) == 0_No + (xR * IxR) by A33, SURREALR:43;
then (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == xR * IxR by A32, SURREALO:4;
then ||.x.|| * yL < xR * IxR by A31, SURREALO:4;
hence ||.x.|| * yL < 1_No by A21, SURREALO:4; :: thesis:

end;

suppose yL in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider yL1 being object such that
A34: ( yL1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . n & yL in divs (yL1,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider yL1 = yL1 as Surreal by A7, A34, A13;
consider xR being object such that
A35: ( xR in L_ ||.x.|| & xR <> 0_No ) and
A36: yL = (1_No +' ((xR +' (-' ||.x.||)) *' yL1)) *' ((No_inverses_on ||.x.||) . xR) by A34, Def2;
reconsider xR = xR as Surreal by A35, SURREAL0:def 16;
A37: xR in (L_ ||.x.||) \/ (R_ ||.x.||) by A35, XBOOLE_0:def 3;
then A38: ( born xR in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A39: xR is positive by A3, A35, Def9;
then reconsider IxR = inv xR as Surreal by A3, A2, A38;
A40: xR * IxR == 1_No by A3, A2, A38, A39;
( ||.x.|| in {||.x.||} & L_ ||.x.|| << {||.x.||} ) by SURREALO:11, TARSKI:def 1;
then A41: xR + (- ||.x.||) < ||.x.|| + (- ||.x.||) by A35, SURREALR:32;
||.x.|| - ||.x.|| == 0_No by SURREALR:39;
then A42: xR + (- ||.x.||) < 0_No by A41, SURREALO:4;
A43: ( (||.x.|| * yL1) * (xR + (- ||.x.||)) < 1_No * (xR + (- ||.x.||)) & 1_No * (xR + (- ||.x.||)) = xR + (- ||.x.||) ) by A12, A34, SURREALR:71, A42;
xR in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A37, A35, ZFMISC_1:56;
then A44: ||.x.|| * yL = ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) by A36, Def13;
A45: ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) == ||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:51, SURREALR:67;
||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:67;
then A46: ||.x.|| * yL == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by A45, A44, SURREALO:4;
A47: 0_No < xR * IxR by SURREALO:4, Def8, A40;
0_No <= xR by A39;
then 0_No < IxR by A47, SURREALR:72;
then A48: ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR < (xR + (- ||.x.||)) * IxR by A43, SURREALR:70;
A49: ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by SURREALR:51, SURREALR:69;
( ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) & (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) ) by SURREALR:69;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) by SURREALO:4;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by A49, SURREALO:4;
then ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) < (xR + (- ||.x.||)) * IxR by A48, SURREALO:4;
then (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) < (||.x.|| * (1_No * IxR)) + ((xR + (- ||.x.||)) * IxR) by SURREALR:44;
then A50: ||.x.|| * yL < (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) by A46, SURREALO:4;
(- ||.x.||) * IxR = - (||.x.|| * IxR) by SURREALR:58;
then (xR + (- ||.x.||)) * IxR == (xR * IxR) + (- (||.x.|| * IxR)) by SURREALR:67;
then A51: (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) by SURREALR:43;
A52: (||.x.|| * IxR) - (||.x.|| * IxR) == 0_No by SURREALR:39;
(||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) = ((||.x.|| * IxR) + (- (||.x.|| * IxR))) + (xR * IxR) by SURREALR:37;
then (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) == 0_No + (xR * IxR) by A52, SURREALR:43;
then (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == 0_No + (xR * IxR) by A51, SURREALO:4;
then ||.x.|| * yL < xR * IxR by A50, SURREALO:4;
hence ||.x.|| * yL < 1_No by A40, SURREALO:4; :: thesis:

end;

suppose yL in (divR (||.x.||,(No_inverses_on ||.x.||))) . n ; :: thesis:

hence 1_No < ||.x.|| * yL by A12; :: thesis:

end;

suppose yL in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider yL1 being object such that
A54: ( yL1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . n & yL in divs (yL1,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider yL1 = yL1 as Surreal by A7, A54, A13;
consider xR being object such that
A55: ( xR in L_ ||.x.|| & xR <> 0_No ) and
A56: yL = (1_No +' ((xR +' (-' ||.x.||)) *' yL1)) *' ((No_inverses_on ||.x.||) . xR) by A54, Def2;
reconsider xR = xR as Surreal by A55, SURREAL0:def 16;
A57: xR in (L_ ||.x.||) \/ (R_ ||.x.||) by A55, XBOOLE_0:def 3;
then A58: ( born xR in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A59: xR is positive by A3, A55, Def9;
then reconsider IxR = inv xR as Surreal by A3, A2, A58;
A60: xR * IxR == 1_No by A3, A2, A58, A59;
( ||.x.|| in {||.x.||} & L_ ||.x.|| << {||.x.||} ) by SURREALO:11, TARSKI:def 1;
then A61: xR + (- ||.x.||) < ||.x.|| + (- ||.x.||) by A55, SURREALR:32;
||.x.|| - ||.x.|| == 0_No by SURREALR:39;
then A62: xR + (- ||.x.||) < 0_No by A61, SURREALO:4;
A63: ( xR + (- ||.x.||) = 1_No * (xR + (- ||.x.||)) & 1_No * (xR + (- ||.x.||)) < (||.x.|| * yL1) * (xR + (- ||.x.||)) ) by A12, A54, SURREALR:71, A62;
xR in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A57, A55, ZFMISC_1:56;
then A64: ||.x.|| * yL = ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) by A56, Def13;
A65: ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) == ||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:51, SURREALR:67;
||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:67;
then A66: ||.x.|| * yL == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by A65, A64, SURREALO:4;
A67: 0_No < xR * IxR by SURREALO:4, Def8, A60;
0_No <= xR by A59;
then 0_No < IxR by A67, SURREALR:72;
then A68: (xR + (- ||.x.||)) * IxR < ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR by A63, SURREALR:70;
A69: ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by SURREALR:51, SURREALR:69;
( ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) & (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) ) by SURREALR:69;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) by SURREALO:4;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by A69, SURREALO:4;
then (xR + (- ||.x.||)) * IxR < ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by A68, SURREALO:4;
then (||.x.|| * (1_No * IxR)) + ((xR + (- ||.x.||)) * IxR) < (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:44;
then A70: (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) < ||.x.|| * yL by A66, SURREALO:4;
(- ||.x.||) * IxR = - (||.x.|| * IxR) by SURREALR:58;
then (xR + (- ||.x.||)) * IxR == (xR * IxR) + (- (||.x.|| * IxR)) by SURREALR:67;
then A71: (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) by SURREALR:43;
A72: (||.x.|| * IxR) - (||.x.|| * IxR) == 0_No by SURREALR:39;
(||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) = ((||.x.|| * IxR) + (- (||.x.|| * IxR))) + (xR * IxR) by SURREALR:37;
then (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) == 0_No + (xR * IxR) by A72, SURREALR:43;
then (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == 0_No + (xR * IxR) by A71, SURREALO:4;
then xR * IxR < ||.x.|| * yL by A70, SURREALO:4;
hence 1_No < ||.x.|| * yL by A60, SURREALO:4; :: thesis:

end;

suppose yL in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider yL1 being object such that
A73: ( yL1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . n & yL in divs (yL1,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider yL1 = yL1 as Surreal by A7, A73, A13;
consider xR being object such that
A74: ( xR in R_ ||.x.|| & xR <> 0_No ) and
A75: yL = (1_No +' ((xR +' (-' ||.x.||)) *' yL1)) *' ((No_inverses_on ||.x.||) . xR) by A73, Def2;
reconsider xR = xR as Surreal by A74, SURREAL0:def 16;
A76: xR in (L_ ||.x.||) \/ (R_ ||.x.||) by A74, XBOOLE_0:def 3;
then A77: ( born xR in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A78: xR is positive by A3, A74, Def9;
then reconsider IxR = inv xR as Surreal by A3, A2, A77;
A79: xR * IxR == 1_No by A3, A2, A77, A78;
( ||.x.|| in {||.x.||} & {||.x.||} << R_ ||.x.|| ) by SURREALO:11, TARSKI:def 1;
then A80: ||.x.|| + (- ||.x.||) < xR + (- ||.x.||) by A74, SURREALR:32;
||.x.|| - ||.x.|| == 0_No by SURREALR:39;
then A81: 0_No < xR + (- ||.x.||) by A80, SURREALO:4;
A82: ( xR + (- ||.x.||) = 1_No * (xR + (- ||.x.||)) & 1_No * (xR + (- ||.x.||)) < (||.x.|| * yL1) * (xR + (- ||.x.||)) ) by A12, A73, A81, SURREALR:70;
xR in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A76, A74, ZFMISC_1:56;
then A83: ||.x.|| * yL = ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) by A75, Def13;
A84: ||.x.|| * ((1_No + ((xR + (- ||.x.||)) * yL1)) * IxR) == ||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:51, SURREALR:67;
||.x.|| * ((1_No * IxR) + (((xR + (- ||.x.||)) * yL1) * IxR)) == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:67;
then A85: ||.x.|| * yL == (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by A84, A83, SURREALO:4;
A86: 0_No < xR * IxR by SURREALO:4, Def8, A79;
0_No <= xR by A78;
then 0_No < IxR by A86, SURREALR:72;
then A87: (xR + (- ||.x.||)) * IxR < ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR by A82, SURREALR:70;
A88: ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by SURREALR:69, SURREALR:51;
( ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) & (||.x.|| * yL1) * ((xR + (- ||.x.||)) * IxR) == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) ) by SURREALR:69;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (yL1 * ((xR + (- ||.x.||)) * IxR)) by SURREALO:4;
then ((||.x.|| * yL1) * (xR + (- ||.x.||))) * IxR == ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by A88, SURREALO:4;
then (xR + (- ||.x.||)) * IxR < ||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR) by A87, SURREALO:4;
then (||.x.|| * (1_No * IxR)) + ((xR + (- ||.x.||)) * IxR) < (||.x.|| * (1_No * IxR)) + (||.x.|| * (((xR + (- ||.x.||)) * yL1) * IxR)) by SURREALR:44;
then A89: (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) < ||.x.|| * yL by A85, SURREALO:4;
(- ||.x.||) * IxR = - (||.x.|| * IxR) by SURREALR:58;
then (xR + (- ||.x.||)) * IxR == (xR * IxR) + (- (||.x.|| * IxR)) by SURREALR:67;
then A90: (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) by SURREALR:43;
A91: (||.x.|| * IxR) - (||.x.|| * IxR) == 0_No by SURREALR:39;
(||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) = ((||.x.|| * IxR) + (- (||.x.|| * IxR))) + (xR * IxR) by SURREALR:37;
then (||.x.|| * IxR) + ((xR * IxR) + (- (||.x.|| * IxR))) == 0_No + (xR * IxR) by A91, SURREALR:43;
then (||.x.|| * IxR) + ((xR + (- ||.x.||)) * IxR) == 0_No + (xR * IxR) by A90, SURREALO:4;
then xR * IxR < ||.x.|| * yL by A89, SURREALO:4;
hence 1_No < ||.x.|| * yL by A79, SURREALO:4; :: thesis:

end;

A92: for n being Nat holds S₂[n] from NAT_1:sch 2(A8, A11);
A93: 0_No <= ||.x.|| by Def8;
A94: Union (divL (||.x.||,(No_inverses_on ||.x.||))) << Union (divR (||.x.||,(No_inverses_on ||.x.||)))

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A95: ( l in Union (divL (||.x.||,(No_inverses_on ||.x.||))) & r in Union (divR (||.x.||,(No_inverses_on ||.x.||))) ) ; :: thesis:
dom (divL (||.x.||,(No_inverses_on ||.x.||))) = NAT by Def5;
then consider n1 being Nat such that
A96: ( l in (divL (||.x.||,(No_inverses_on ||.x.||))) . n1 & ( for m being Nat st l in (divL (||.x.||,(No_inverses_on ||.x.||))) . m holds
n1 <= m ) ) by A95, Th27;
dom (divR (||.x.||,(No_inverses_on ||.x.||))) = NAT by Def6;
then consider n2 being Nat such that
A97: ( r in (divR (||.x.||,(No_inverses_on ||.x.||))) . n2 & ( for m being Nat st r in (divR (||.x.||,(No_inverses_on ||.x.||))) . m holds
n2 <= m ) ) by A95, Th27;
n2 <> 0 by A97, Th1;
then reconsider N2 = n2 - 1 as Nat by NAT_1:20;

suppose n1 = 0 ; :: thesis:

then {0_No} = (divL (||.x.||,(No_inverses_on ||.x.||))) . n1 by Th1;
then A98: l = 0_No by A96, TARSKI:def 1;
( 0_No <= 1_No & 1_No < ||.x.|| * r ) by A92, A97, Def8;
then 0_No < ||.x.|| * r by SURREALO:4;
hence not r <= l by A98, A93, SURREALR:72; :: thesis:

end;

suppose 0 < n1 ; :: thesis:

suppose l in (divL (||.x.||,(No_inverses_on ||.x.||))) . N1 ; :: thesis:

then N1 >= N1 + 1 by A96;
hence not r <= l by NAT_1:13; :: thesis:

end;

suppose l in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N1),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y1 being object such that
A100: ( y1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . N1 & l in divs (y1,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y1 = y1 as Surreal by A100, A99, A7;
consider x1 being object such that
A101: ( x1 in R_ ||.x.|| & x1 <> 0_No & l = (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' ((No_inverses_on ||.x.||) . x1) ) by A100, Def2;
reconsider x1 = x1 as Surreal by A101, SURREAL0:def 16;
A102: ( x1 is positive & x1 in R_ x ) by A3, Def9, A101;
then ( 0_No < x1 & x1 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A103: born x1 in born x by SURREALO:1;
then reconsider Ix1 = inv x1 as Surreal by A102, A3, A2;
A104: x1 * Ix1 == 1_No by A3, A2, A103, A102;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A101, XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A101, ZFMISC_1:56;
then A105: Ix1 = (No_inverses_on ||.x.||) . x1 by Def13;
(divR (||.x.||,(No_inverses_on ||.x.||))) . (N2 + 1) = (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||))) by Th6;
then ( r in ((divR (||.x.||,(No_inverses_on ||.x.||))) . N2) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) or r in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by A97, XBOOLE_0:def 3;

suppose r in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 ; :: thesis:

then N2 >= N2 + 1 by A97;
hence not r <= l by NAT_1:13; :: thesis:

end;

suppose r in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A106: ( y2 in (divL (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A106, A99;
consider x2 being object such that
A107: ( x2 in L_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A106, Def2;
reconsider x2 = x2 as Surreal by A107, SURREAL0:def 16;
A108: ( x2 is positive & x2 in L_ x ) by A3, Def9, A107;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A109: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A108, A3, A2;
A110: x2 * Ix2 == 1_No by A3, A2, A109, A108;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A107, XBOOLE_0:def 3;
then A111: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A107, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A112: ( 0_No < x1 - ||.x.|| & 0_No < ||.x.|| - x2 ) by SURREALR:45, A101, A107;
L_ ||.x.|| << R_ ||.x.|| by SURREAL0:45;
then A113: 0_No < x1 - x2 by A107, A101, SURREALR:45;
A114: ( 0_No < 1_No - (||.x.|| * y1) & 0_No < 1_No - (||.x.|| * y2) ) by A100, A106, A92, SURREALR:45;
A115: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A116: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A117: ( x2 is positive & x1 is positive ) by A3, A107, A101, Def9;
A118: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A113, A114, SURREALR:72;
A119: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A113, A114, SURREALR:72;

suppose y1 == y2 ; :: thesis:

then ( y1 + (- y2) == y2 - y2 & y2 - y2 == 0_No ) by SURREALR:43, SURREALR:39;
then y1 + (- y2) == 0_No by SURREALO:4;
then ( (y1 + (- y2)) * x1 == 0_No * x1 & 0_No * x1 = 0_No ) by SURREALR:51;
then ( ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) == 0_No * (||.x.|| + (- x2)) & 0_No * (||.x.|| + (- x2)) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A118, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A115, SURREALO:4; :: thesis:

end;

suppose y1 < y2 ; :: thesis:

then 0_No < y2 - y1 by SURREALR:45;
then 0_No < (y2 + (- y1)) * x2 by A117, SURREALR:72;
then 0_No <= ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A112, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A119, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A116, SURREALO:4; :: thesis:

end;

suppose y2 < y1 ; :: thesis:

then 0_No < y1 - y2 by SURREALR:45;
then 0_No < (y1 + (- y2)) * x1 by A117, SURREALR:72;
then 0_No <= ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A112, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A118, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A115, SURREALO:4; :: thesis:

end;

then (1_No + ((x1 + (- ||.x.||)) * y1)) * x2 < (1_No + ((x2 + (- ||.x.||)) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1 < (1_No + ((x2 + (- ||.x.||)) * y2)) * Ix2 by A108, A102, A104, A110, Th28;
hence not r <= l by A101, A107, A105, A111, Def13; :: thesis:

end;

suppose r in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A120: ( y2 in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A120, A99;
consider x2 being object such that
A121: ( x2 in R_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A120, Def2;
reconsider x2 = x2 as Surreal by A121, SURREAL0:def 16;
A122: ( x2 is positive & x2 in R_ x ) by A3, Def9, A121;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A123: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A122, A3, A2;
A124: x2 * Ix2 == 1_No by A3, A2, A123, A122;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A121, XBOOLE_0:def 3;
then A125: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A121, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A126: ( 0_No < x1 - ||.x.|| & ||.x.|| - x2 < 0_No ) by A101, A121, SURREALR:45, SURREALR:46;
( ||.x.|| * y1 < 1_No & 1_No <= ||.x.|| * y2 ) by A100, A120, A92;
then ||.x.|| * y1 < ||.x.|| * y2 by SURREALO:4;
then y1 < y2 by Def8, SURREALR:73;
then A127: ( y1 - y2 < 0_No & 0_No < y2 - y1 ) by SURREALR:45, SURREALR:46;
A128: 1_No - (||.x.|| * y2) < 0_No by A120, A92, SURREALR:46;
A129: ( 0_No < 1_No - (||.x.|| * y1) & 0_No < (||.x.|| * y2) - 1_No ) by A100, A120, A92, SURREALR:45;
A130: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A131: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A132: ( x2 is positive & x1 is positive ) by A3, A121, A101, Def9;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

A133: ((y1 + (- y2)) * (||.x.|| + (- x2))) * x1 == ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by SURREALR:69;
0_No < (y1 + (- y2)) * (||.x.|| + (- x2)) by A127, A126, SURREALR:72;
then 0_No < ((y1 + (- y2)) * (||.x.|| + (- x2))) * x1 by A132, SURREALR:72;
then A134: 0_No < ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A133, SURREALO:4;

suppose x2 < x1 ; :: thesis:

then 0_No < x1 - x2 by SURREALR:45;
then A135: 0_No <= (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A129, SURREALR:72;
0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A134, A135, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A130, SURREALO:4; :: thesis:

end;

suppose x1 == x2 ; :: thesis:

then ( x1 + (- x2) == x2 + (- x2) & x2 + (- x2) = x2 - x2 & x2 - x2 == 0_No ) by SURREALR:43, SURREALR:39;
then x1 + (- x2) == 0_No by SURREALO:4;
then ( (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) == 0_No * (1_No + (- (||.x.|| * y1))) & 0_No * (1_No + (- (||.x.|| * y1))) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A134, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A130, SURREALO:4; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

then x1 - x2 < 0_No by SURREALR:46;
then A136: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A128, SURREALR:72;
0_No < (y2 + (- y1)) * x2 by A127, A132, SURREALR:72;
then 0_No <= ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A126, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A136, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A131, SURREALO:4; :: thesis:

end;

hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) ; :: thesis:

end;

then (1_No + ((x1 + (- ||.x.||)) * y1)) * x2 < (1_No + ((x2 + (- ||.x.||)) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1 < (1_No + ((x2 + (- ||.x.||)) * y2)) * Ix2 by A122, A102, A104, A124, Th28;
hence not r <= l by A101, A121, A105, A125, Def13; :: thesis:

end;

suppose l in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N1),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y1 being object such that
A137: ( y1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . N1 & l in divs (y1,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y1 = y1 as Surreal by A137, A99, A7;
consider x1 being object such that
A138: ( x1 in L_ ||.x.|| & x1 <> 0_No & l = (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' ((No_inverses_on ||.x.||) . x1) ) by A137, Def2;
reconsider x1 = x1 as Surreal by A138, SURREAL0:def 16;
A139: ( x1 is positive & x1 in L_ x ) by A3, Def9, A138;
then ( 0_No < x1 & x1 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A140: born x1 in born x by SURREALO:1;
then reconsider Ix1 = inv x1 as Surreal by A139, A3, A2;
A141: x1 * Ix1 == 1_No by A3, A2, A140, A139;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A138, XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A138, ZFMISC_1:56;
then A142: Ix1 = (No_inverses_on ||.x.||) . x1 by Def13;
(divR (||.x.||,(No_inverses_on ||.x.||))) . (N2 + 1) = (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||))) by Th6;
then ( r in ((divR (||.x.||,(No_inverses_on ||.x.||))) . N2) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) or r in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by A97, XBOOLE_0:def 3;

suppose r in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 ; :: thesis:

then N2 >= N2 + 1 by A97;
hence not r <= l by NAT_1:13; :: thesis:

end;

suppose r in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A143: ( y2 in (divL (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A143, A99;
consider x2 being object such that
A144: ( x2 in L_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A143, Def2;
reconsider x2 = x2 as Surreal by A144, SURREAL0:def 16;
A145: ( x2 is positive & x2 in L_ x ) by A3, Def9, A144;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A146: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A145, A3, A2;
A147: x2 * Ix2 == 1_No by A3, A2, A146, A145;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A144, XBOOLE_0:def 3;
then A148: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A144, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A149: ( x1 - ||.x.|| < 0_No & x2 - ||.x.|| < 0_No & 0_No < ||.x.|| - x2 ) by A138, A144, SURREALR:45, SURREALR:46;
( ||.x.|| * y2 < 1_No & 1_No <= ||.x.|| * y1 ) by A137, A143, A92;
then ||.x.|| * y2 < ||.x.|| * y1 by SURREALO:4;
then y2 < y1 by Def8, SURREALR:73;
then A150: ( y2 - y1 < 0_No & 0_No < y1 - y2 ) by SURREALR:45, SURREALR:46;
A151: 0_No < 1_No - (||.x.|| * y2) by A143, A92, SURREALR:45;
A152: ( 1_No - (||.x.|| * y1) < 0_No & (||.x.|| * y2) - 1_No < 0_No ) by A137, A143, A92, SURREALR:46;
A153: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A154: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A155: ( x2 is positive & x1 is positive ) by A3, A144, A138, Def9;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

A156: ((y2 + (- y1)) * (x1 + (- ||.x.||))) * x2 == ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by SURREALR:69;
0_No < (y2 + (- y1)) * (x1 + (- ||.x.||)) by A150, A149, SURREALR:72;
then 0_No < ((y2 + (- y1)) * (x1 + (- ||.x.||))) * x2 by A155, SURREALR:72;
then A157: 0_No < ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A156, SURREALO:4;

suppose x2 < x1 ; :: thesis:

then 0_No < x1 - x2 by SURREALR:45;
then A158: 0_No <= (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A151, SURREALR:72;
( 0_No = 0_No + 0_No & 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) ) by A157, A158, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A154, SURREALO:4; :: thesis:

end;

suppose x1 == x2 ; :: thesis:

then ( x1 + (- x2) == x2 - x2 & x2 - x2 == 0_No ) by SURREALR:43, SURREALR:39;
then x1 + (- x2) == 0_No by SURREALO:4;
then ( (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) == 0_No * (1_No + (- (||.x.|| * y2))) & 0_No * (1_No + (- (||.x.|| * y2))) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A157, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A154, SURREALO:4; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

then x1 - x2 < 0_No by SURREALR:46;
then A159: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A152, SURREALR:72;
0_No < (y1 + (- y2)) * x1 by A150, A155, SURREALR:72;
then 0_No <= ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A149, SURREALR:72;
then ( 0_No = 0_No + 0_No & 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) ) by A159, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A153, SURREALO:4; :: thesis:

end;

hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) ; :: thesis:

end;

then (1_No + ((x1 - ||.x.||) * y1)) * x2 < (1_No + ((x2 - ||.x.||) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 - ||.x.||) * y1)) * Ix1 < (1_No + ((x2 - ||.x.||) * y2)) * Ix2 by A145, A139, A141, A147, Th28;
hence not r <= l by A138, A144, A142, A148, Def13; :: thesis:

end;

suppose r in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . N2),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ; :: thesis:

then consider y2 being object such that
A160: ( y2 in (divR (||.x.||,(No_inverses_on ||.x.||))) . N2 & r in divs (y2,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) ) by Def3;
reconsider y2 = y2 as Surreal by A7, A160, A99;
consider x2 being object such that
A161: ( x2 in R_ ||.x.|| & x2 <> 0_No & r = (1_No +' ((x2 +' (-' ||.x.||)) *' y2)) *' ((No_inverses_on ||.x.||) . x2) ) by A160, Def2;
reconsider x2 = x2 as Surreal by A161, SURREAL0:def 16;
A162: ( x2 is positive & x2 in R_ x ) by A3, Def9, A161;
then ( 0_No < x2 & x2 in (L_ x) \/ (R_ x) ) by XBOOLE_0:def 3;
then A163: born x2 in born x by SURREALO:1;
then reconsider Ix2 = inv x2 as Surreal by A162, A3, A2;
A164: x2 * Ix2 == 1_No by A3, A2, A163, A162;
x2 in (L_ ||.x.||) \/ (R_ ||.x.||) by A161, XBOOLE_0:def 3;
then A165: x2 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A161, ZFMISC_1:56;
0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2)

( L_ ||.x.|| << {||.x.||} & {||.x.||} << R_ ||.x.|| & ||.x.|| in {||.x.||} ) by TARSKI:def 1, SURREALO:11;
then A166: ( x1 - ||.x.|| < 0_No & 0_No < ||.x.|| - x1 & ||.x.|| - x2 < 0_No & 0_No < x2 - ||.x.|| ) by A138, A161, SURREALR:45, SURREALR:46;
L_ ||.x.|| << R_ ||.x.|| by SURREAL0:45;
then A167: x1 - x2 < 0_No by A161, A138, SURREALR:46;
A168: ( 1_No - (||.x.|| * y1) < 0_No & 1_No - (||.x.|| * y2) < 0_No ) by A137, A160, A92, SURREALR:46;
A169: ((1_No + ((x2 - ||.x.||) * y2)) * x1) + (- ((1_No + ((x1 - ||.x.||) * y1)) * x2)) == ((x1 - x2) * (1_No - (||.x.|| * y1))) + (((y1 - y2) * x1) * (||.x.|| - x2)) by Th29;
A170: ((1_No + ((x2 - ||.x.||) * y2)) * x1) - ((1_No + ((x1 - ||.x.||) * y1)) * x2) == ((x1 - x2) * (1_No - (||.x.|| * y2))) + (((y2 - y1) * x2) * (x1 - ||.x.||)) by Th29;
A171: ( x2 is positive & x1 is positive ) by A3, A161, A138, Def9;
A172: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y1))) by A167, A168, SURREALR:72;
A173: 0_No < (x1 + (- x2)) * (1_No + (- (||.x.|| * y2))) by A167, A168, SURREALR:72;

suppose y1 == y2 ; :: thesis:

then ( y1 + (- y2) == y2 - y2 & y2 - y2 == 0_No ) by SURREALR:43, SURREALR:39;
then y1 + (- y2) == 0_No by SURREALO:4;
then ( (y1 + (- y2)) * x1 == 0_No * x1 & 0_No * x1 = 0_No ) by SURREALR:51;
then ( ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) == 0_No * (||.x.|| + (- x2)) & 0_No * (||.x.|| + (- x2)) = 0_No ) by SURREALR:51;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) by A172, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A169, SURREALO:4; :: thesis:

end;

suppose y1 < y2 ; :: thesis:

then y1 - y2 < 0_No by SURREALR:46;
then (y1 + (- y2)) * x1 < 0_No by A171, SURREALR:74;
then 0_No <= ((y1 + (- y2)) * x1) * (||.x.|| + (- x2)) by A166, SURREALR:72;
then ( 0_No = 0_No + 0_No & 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y1)))) + (((y1 + (- y2)) * x1) * (||.x.|| + (- x2))) ) by A172, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A169, SURREALO:4; :: thesis:

end;

suppose y2 < y1 ; :: thesis:

then y2 - y1 < 0_No by SURREALR:46;
then (y2 + (- y1)) * x2 < 0_No by A171, SURREALR:74;
then 0_No <= ((y2 + (- y1)) * x2) * (x1 + (- ||.x.||)) by A166, SURREALR:72;
then 0_No + 0_No < ((x1 + (- x2)) * (1_No + (- (||.x.|| * y2)))) + (((y2 + (- y1)) * x2) * (x1 + (- ||.x.||))) by A173, SURREALR:44;
hence 0_No < ((1_No + ((x2 + (- ||.x.||)) * y2)) * x1) - ((1_No + ((x1 + (- ||.x.||)) * y1)) * x2) by A170, SURREALO:4; :: thesis:

end;

then (1_No + ((x1 - ||.x.||) * y1)) * x2 < (1_No + ((x2 - ||.x.||) * y2)) * x1 by SURREALR:45;
then (1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1 < (1_No + ((x2 + (- ||.x.||)) * y2)) * Ix2 by A162, A139, A141, A164, Th28;
hence not r <= l by A138, A161, A142, A165, Def13; :: thesis:

end;

reconsider UL = Union (divL (||.x.||,(No_inverses_on ||.x.||))), UR = Union (divR (||.x.||,(No_inverses_on ||.x.||))) as surreal-membered set by A5, Th10;
consider M being Ordinal such that
A174: for o being object st o in UL \/ UR holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
A175: inv x = [UL,UR] by A3, Th26;
inv x in Day M by A175, A174, A94, SURREAL0:46;
hence inv x is surreal ; :: thesis:
let y be Surreal; :: thesis:
assume A176: y = inv x ; :: thesis:
set xy = ||.x.|| * y;
A177: ||.x.|| * y = [((comp ((L_ ||.x.||),||.x.||,y,(L_ y))) \/ (comp ((R_ ||.x.||),||.x.||,y,(R_ y)))),((comp ((L_ ||.x.||),||.x.||,y,(R_ y))) \/ (comp ((R_ ||.x.||),||.x.||,y,(L_ y))))] by SURREALR:50;
A178: ( UL = L_ y & L_ y << {y} & {y} << R_ y & R_ y = UR & y in {y} ) by SURREALO:11, A175, A176, TARSKI:def 1;
A179: ( dom (divL (||.x.||,(No_inverses_on ||.x.||))) = NAT & NAT = dom (divR (||.x.||,(No_inverses_on ||.x.||))) ) by Def5, Def6;
A180: {1_No} << R_ (||.x.|| * y)

let r, l be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A181: ( r in {1_No} & l in R_ (||.x.|| * y) ) ; :: thesis:

per cases by A177, A181, XBOOLE_0:def 3;

suppose l in comp ((L_ ||.x.||),||.x.||,y,(R_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A182: ( l = ((x1 * y) +' (||.x.|| * y1)) +' (-' (x1 * y1)) & x1 in L_ ||.x.|| & y1 in R_ y ) by SURREALR:def 14;
consider n being Nat such that
A183: ( y1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . n & ( for m being Nat st y1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . m holds
n <= m ) ) by A182, A175, A176, Th27, A179;

suppose x1 = 0_No ; :: thesis:

then A184: l = (0_No + (||.x.|| * y1)) + 0_No by SURREALR:23, A182;
1_No < ||.x.|| * y1 by A183, A92;
hence not l <= r by A184, A181, TARSKI:def 1; :: thesis:

end;

suppose A185: x1 <> 0_No ; :: thesis:

x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A182, XBOOLE_0:def 3;
then A186: ( born x1 in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A187: x1 is positive by A3, A185, A182, Def9;
then reconsider Ix1 = inv x1 as Surreal by A3, A2, A186;
x1 * Ix1 == 1_No by A3, A2, A186, A187;
then A188: ((x1 * y) + (||.x.|| * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - ||.x.||) * y1)) * Ix1))) by Th30;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A182, XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A185, ZFMISC_1:56;
then Ix1 = (No_inverses_on ||.x.||) . x1 by Def13;
then (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' Ix1 in divs (y1,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) by A185, A182, Def2;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) by A183, Def3;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (((divL (||.x.||,(No_inverses_on ||.x.||))) . n) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then A189: (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . (n + 1) by Th6;
(1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in UL by A179, A189, CARD_5:2;
then 0_No < y - ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1) by A178, SURREALR:45;
then 0_No < x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1))) by A187, SURREALR:72;
then 1_No + 0_No < 1_No + (x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1)))) by SURREALR:44;
then ( 1_No = 1_No + 0_No & 1_No + 0_No < l ) by A182, A188, SURREALO:4;
hence not l <= r by A181, TARSKI:def 1; :: thesis:

end;

suppose l in comp ((R_ ||.x.||),||.x.||,y,(L_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A190: ( l = ((x1 * y) +' (||.x.|| * y1)) +' (-' (x1 * y1)) & x1 in R_ ||.x.|| & y1 in L_ y ) by SURREALR:def 14;
consider n being Nat such that
A191: ( y1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . n & ( for m being Nat st y1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . m holds
n <= m ) ) by A190, A175, A176, Th27, A179;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A190, XBOOLE_0:def 3;
then A192: ( born x1 in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A193: x1 is positive by A3, A190, Def9;
then reconsider Ix1 = inv x1 as Surreal by A3, A2, A192;
x1 * Ix1 == 1_No by A3, A2, A192, A193;
then A194: ((x1 * y) + (||.x.|| * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - ||.x.||) * y1)) * Ix1))) by Th30;
A195: ( 0_No <= 0_No & 0_No < x1 ) by A193;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A190, XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A195, ZFMISC_1:56;
then Ix1 = (No_inverses_on ||.x.||) . x1 by Def13;
then (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' Ix1 in divs (y1,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) by A195, A190, Def2;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) by A191, Def3;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in ((divL (||.x.||,(No_inverses_on ||.x.||))) . n) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (((divL (||.x.||,(No_inverses_on ||.x.||))) . n) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then A196: (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . (n + 1) by Th6;
(1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in UL by A179, A196, CARD_5:2;
then 0_No < y - ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1) by A178, SURREALR:45;
then 0_No < x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1))) by A193, SURREALR:72;
then 1_No + 0_No < 1_No + (x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1)))) by SURREALR:44;
then ( 1_No = 1_No + 0_No & 1_No + 0_No < l ) by A194, A190, SURREALO:4;
hence not l <= r by A181, TARSKI:def 1; :: thesis:

end;

A197: L_ (||.x.|| * y) << {1_No}

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A198: ( l in L_ (||.x.|| * y) & r in {1_No} ) ; :: thesis:

per cases by A177, A198, XBOOLE_0:def 3;

suppose l in comp ((L_ ||.x.||),||.x.||,y,(L_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A199: ( l = ((x1 * y) +' (||.x.|| * y1)) +' (-' (x1 * y1)) & x1 in L_ ||.x.|| & y1 in L_ y ) by SURREALR:def 14;
consider n being Nat such that
A200: ( y1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . n & ( for m being Nat st y1 in (divL (||.x.||,(No_inverses_on ||.x.||))) . m holds
n <= m ) ) by A199, A175, A176, Th27, A179;

suppose x1 = 0_No ; :: thesis:

then A201: l = (0_No + (||.x.|| * y1)) + 0_No by SURREALR:23, A199;
||.x.|| * y1 < 1_No by A92, A200;
hence not r <= l by A201, A198, TARSKI:def 1; :: thesis:

end;

suppose A202: x1 <> 0_No ; :: thesis:

x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A199, XBOOLE_0:def 3;
then A203: ( born x1 in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A204: x1 is positive by A3, A202, A199, Def9;
then reconsider Ix1 = inv x1 as Surreal by A3, A2, A203;
x1 * Ix1 == 1_No by A3, A2, A203, A204;
then A205: ((x1 * y) + (||.x.|| * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - ||.x.||) * y1)) * Ix1))) by Th30;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A199, XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A202, ZFMISC_1:56;
then Ix1 = (No_inverses_on ||.x.||) . x1 by Def13;
then (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' Ix1 in divs (y1,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) by A202, A199, Def2;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) by A200, Def3;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in ((divR (||.x.||,(No_inverses_on ||.x.||))) . n) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (((divR (||.x.||,(No_inverses_on ||.x.||))) . n) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then A206: (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . (n + 1) by Th6;
(1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in UR by A179, A206, CARD_5:2;
then y - ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1) < 0_No by A178, SURREALR:46;
then x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1))) < 0_No by A204, SURREALR:74;
then 1_No + (x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1)))) < 1_No + 0_No by SURREALR:44;
then ( l < 1_No + 0_No & 1_No + 0_No = 1_No ) by A199, A205, SURREALO:4;
hence not r <= l by A198, TARSKI:def 1; :: thesis:

end;

suppose l in comp ((R_ ||.x.||),||.x.||,y,(R_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A207: ( l = ((x1 * y) +' (||.x.|| * y1)) +' (-' (x1 * y1)) & x1 in R_ ||.x.|| & y1 in R_ y ) by SURREALR:def 14;
consider n being Nat such that
A208: ( y1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . n & ( for m being Nat st y1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . m holds
n <= m ) ) by A207, A175, A176, Th27, A179;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A207, XBOOLE_0:def 3;
then A209: ( born x1 in born ||.x.|| & born ||.x.|| c= born x ) by A3, SURREALO:1, Th22;
A210: x1 is positive by A3, A207, Def9;
then reconsider Ix1 = inv x1 as Surreal by A3, A2, A209;
x1 * Ix1 == 1_No by A3, A2, A209, A210;
then A211: ((x1 * y) + (||.x.|| * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - ||.x.||) * y1)) * Ix1))) by Th30;
A212: ( 0_No <= 0_No & 0_No < x1 ) by A210;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by A207, XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A212, ZFMISC_1:56;
then Ix1 = (No_inverses_on ||.x.||) . x1 by Def13;
then (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' Ix1 in divs (y1,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) by A212, A207, Def2;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) by A208, Def3;
then (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (((divR (||.x.||,(No_inverses_on ||.x.||))) . n) \/ (divset (((divL (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (((divR (||.x.||,(No_inverses_on ||.x.||))) . n),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then A213: (1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in (divR (||.x.||,(No_inverses_on ||.x.||))) . (n + 1) by Th6;
(1_No + ((x1 + (- ||.x.||)) * y1)) *' Ix1 in UR by A179, A213, CARD_5:2;
then y - ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1) < 0_No by A178, SURREALR:46;
then x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1))) < 0_No by A210, SURREALR:74;
then 1_No + (x1 * (y + (- ((1_No + ((x1 + (- ||.x.||)) * y1)) * Ix1)))) < 1_No + 0_No by SURREALR:44;
then ( l < 1_No + 0_No & 1_No + 0_No = 1_No ) by A207, A211, SURREALO:4;
hence not r <= l by A198, TARSKI:def 1; :: thesis:

end;

A214: (R_ 1_No) \/ (R_ (||.x.|| * y)) = R_ (||.x.|| * y) ;
reconsider oxy = [((L_ 1_No) \/ (L_ (||.x.|| * y))),(R_ (||.x.|| * y))] as Surreal by A180, A197, A214, SURREALO:14;
A215: 0_No in L_ ||.x.|| by A3, Def9;
0_No in {0_No} by TARSKI:def 1;
then 0_No in {0_No} \/ (divset (UL,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then 0_No in ({0_No} \/ (divset (UL,||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset (UR,||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||))) by XBOOLE_0:def 3;
then A216: 0_No in L_ y by A176, A175, Th12;
((0_No * y) + (||.x.|| * 0_No)) + (- (0_No * 0_No)) = 0_No ;
then 0_No in comp ((L_ ||.x.||),||.x.||,y,(L_ y)) by A216, A215, SURREALR:def 14;
then 0_No in (comp ((L_ ||.x.||),||.x.||,y,(L_ y))) \/ (comp ((R_ ||.x.||),||.x.||,y,(R_ y))) by XBOOLE_0:def 3;
then ||.x.|| * y = oxy by A177, ZFMISC_1:40;
then A217: ||.x.|| * y == 1_No by A180, A197, A214, SURREALO:15;
x * y == ||.x.|| * y by A3, Th18, SURREALR:51;
hence x * y == 1_No by A217, SURREALO:4; :: thesis:

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence for x being Surreal st x is positive holds
( inv x is surreal & ( for y being Surreal st y = inv x holds
x * y == 1_No ) ) ; :: thesis:

end;

registration

let x be positive Surreal;

cluster inv x -> surreal ;

coherence by Lm2;

end;

theorem :: SURREALI:31

for x being Surreal st x is positive holds
inv x is Surreal ;

theorem :: SURREALI:32

for x, y being Surreal st x is positive & y = inv x holds
x * y == 1_No by Lm2;

definition

let x be Surreal;
assume A1: not x == 0_No ;

func x " -> Surreal means :Def14: :: SURREALI:def 14
it = inv x if x is positive
otherwise - it = inv (- x);

thus ( x is positive implies ex IT being Surreal st IT = inv x ) ; :: thesis:
assume not x is positive ; :: thesis:
then - x is positive by A1, SURREALR:10, SURREALR:23;
then reconsider i = inv (- x) as Surreal ;
- (- i) = i ;
hence ex b₁ being Surreal st - b₁ = inv (- x) ; :: thesis:

end;

let I1, I2 be Surreal; :: thesis:
( I1 = - (- I1) & I2 = - (- I2) ) ;
hence ( ( x is positive & I1 = inv x & I2 = inv x implies I1 = I2 ) & ( not x is positive & - I1 = inv (- x) & - I2 = inv (- x) implies I1 = I2 ) ) ; :: thesis:

end;

correctness ;

end;

:: deftheorem Def14 defines " SURREALI:def 14 :

theorem Th33: :: SURREALI:33

for x being Surreal st not x == 0_No holds
x * (x ") == 1_No

let x be Surreal; :: thesis:
assume A1: not x == 0_No ; :: thesis:

suppose 0_No < x ; :: thesis:

then A2: x is positive ;
then x " = inv x by A1, Def14;
hence x * (x ") == 1_No by A2, Lm2; :: thesis:

end;

suppose A3: not 0_No < x ; :: thesis:

then A4: - x is positive by A1, SURREALR:23, SURREALR:10;
then reconsider I = inv (- x) as Surreal ;
A5: not x is positive by A3;
(x ") * x = - (- ((x ") * x))
.= (- (x ")) * (- x) by SURREALR:58
.= I * (- x) by A5, A1, Def14 ;
hence x * (x ") == 1_No by A4, Lm2; :: thesis:

end;

definition

let X, Y be set ;
let x be Surreal;

func divset (X,x,Y) -> set means :Def15: :: SURREALI:def 15
for o being object holds
( o in it iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) );

defpred S₁[ object , object ] means ( $1 is pair & L_ $1 is surreal & R_ $1 is surreal & ( for x1, y1 being Surreal st $1 = [x1,y1] holds
( 0_No < x1 & $2 = (1_No + ((x1 + (- x)) * y1)) * (x1 ") ) ) );
A1: for a, b, c being object st S₁[a,b] & S₁[a,c] holds
b = c

let a, b, c be object ; :: thesis:
assume A2: ( S₁[a,b] & S₁[a,c] ) ; :: thesis:
consider a1, a2 being object such that
A3: a = [a1,a2] by XTUPLE_0:def 1, A2;
reconsider a1 = a1, a2 = a2 as Surreal by A3, A2;
thus b = (1_No + ((a1 + (- x)) * a2)) * (a1 ") by A3, A2
.= c by A3, A2 ; :: thesis:

end;

consider D being set such that
A4: for x being object holds
( x in D iff ex y being object st
( y in [:X,Y:] & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take D ; :: thesis:
let o be object ; :: thesis:
thus ( o in D implies ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) :: thesis:

assume o in D ; :: thesis:
then consider y being object such that
A5: ( y in [:X,Y:] & S₁[y,o] ) by A4;
consider a1, a2 being object such that
A6: y = [a1,a2] by XTUPLE_0:def 1, A5;
reconsider a1 = a1, a2 = a2 as Surreal by A6, A5;
take a1 ; :: thesis:
take a2 ; :: thesis:
thus ( 0_No < a1 & a1 in X & a2 in Y & o = (1_No + ((a1 - x) * a2)) * (a1 ") ) by A6, A5, ZFMISC_1:87; :: thesis:

end;

given x1, y1 being Surreal such that A7: ( 0_No < x1 & x1 in X & y1 in Y ) and
A8: o = (1_No + ((x1 - x) * y1)) * (x1 ") ; :: thesis:
A9: [x1,y1] in [:X,Y:] by A7, ZFMISC_1:87;
S₁[[x1,y1],o]

thus ( [x1,y1] is pair & L_ [x1,y1] is surreal & R_ [x1,y1] is surreal ) ; :: thesis:
let X1, Y1 be Surreal; :: thesis:
assume [x1,y1] = [X1,Y1] ; :: thesis:
then ( x1 = X1 & y1 = Y1 ) by XTUPLE_0:1;
hence ( 0_No < X1 & o = (1_No + ((X1 + (- x)) * Y1)) * (X1 ") ) by A7, A8; :: thesis:

end;

hence o in D by A9, A4; :: thesis:

end;

let D1, D2 be set ; :: thesis:
assume that
A10: for o being object holds
( o in D1 iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) and
A11: for o being object holds
( o in D2 iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
( o in D1 iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) by A10;
hence ( o in D1 iff o in D2 ) by A11; :: thesis:

end;

hence D1 = D2 by TARSKI:2; :: thesis:

end;

:: deftheorem Def15 defines divset SURREALI:def 15 :

registration

let X, Y be set ;
let x be Surreal;

cluster divset (X,x,Y) -> surreal-membered ;

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in divset (X,x,Y) ; :: thesis:
then ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) by Def15;
hence o is surreal ; :: thesis:

end;

theorem Th34: :: SURREALI:34

for x being Surreal
for X, nX being set
for Y being surreal-membered set st x is positive & ( ( X = L_ x & nX = L_ ||.x.|| ) or ( X = R_ x & nX = R_ ||.x.|| ) ) holds
divset (X,||.x.||,Y) = divset (Y,||.x.||,nX,(No_inverses_on ||.x.||))

let x be Surreal; :: thesis:
set Nx = ||.x.||;
set Inv = No_inverses_on ||.x.||;
let X, X1 be set ; :: thesis:
let Y be surreal-membered set ; :: thesis:
assume that
A1: x is positive and
A2: ( ( X = L_ x & X1 = L_ ||.x.|| ) or ( X = R_ x & X1 = R_ ||.x.|| ) ) ; :: thesis:
thus divset (X,||.x.||,Y) c= divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) :: according to XBOOLE_0:def 10 :: thesis:

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset (X,||.x.||,Y) ; :: thesis:
then consider x1, y1 being Surreal such that
A3: ( 0_No < x1 & x1 in X & y1 in Y ) and
A4: o = (1_No + ((x1 - ||.x.||) * y1)) * (x1 ") by Def15;
A5: x1 is positive by A3;
not x1 == 0_No by A3;
then A6: x1 " = inv x1 by A5, Def14;
A7: x1 is positive by A3;
A8: 0_No <= 0_No ;
A9: x1 in X1 by A2, A3, A1, A7, Def9;
( x1 in L_ ||.x.|| or x1 in R_ ||.x.|| ) by A2, A3, A1, A7, Def9;
then x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A8, A3, ZFMISC_1:56;
then o = (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' ((No_inverses_on ||.x.||) . x1) by A6, A4, Def13;
then o in divs (y1,||.x.||,X1,(No_inverses_on ||.x.||)) by A9, A8, A3, Def2;
hence o in divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) by A3, Def3; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) ; :: thesis:
then consider y1 being object such that
A10: ( y1 in Y & o in divs (y1,||.x.||,X1,(No_inverses_on ||.x.||)) ) by Def3;
reconsider y1 = y1 as Surreal by A10, SURREAL0:def 16;
consider x1 being object such that
A11: ( x1 in X1 & x1 <> 0_No & o = (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' ((No_inverses_on ||.x.||) . x1) ) by A10, Def2;
reconsider x1 = x1 as Surreal by A2, A11, SURREAL0:def 16;
A12: ( x1 in X & x1 is positive ) by A2, A1, A11, Def9;
A13: not x1 == 0_No by A12;
A14: x1 " = inv x1 by A12, A13, Def14;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by XBOOLE_0:def 3, A2, A11;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A11, ZFMISC_1:56;
then o = (1_No + ((x1 - ||.x.||) * y1)) * (x1 ") by A11, A14, Def13;
hence o in divset (X,||.x.||,Y) by Def15, A12, A10; :: thesis:

end;

theorem Th35: :: SURREALI:35

for x, y being Surreal
for X, Y being set st x == y holds
divset (X,x,Y) <=_ divset (X,y,Y)

let x, y be Surreal; :: thesis:
let X, Y be set ; :: thesis:
assume A1: x == y ; :: thesis:
let z be Surreal; :: according to SURREALO:def 3 :: thesis:
assume z in divset (X,x,Y) ; :: thesis:
then consider x1, y1 being Surreal such that
A2: ( 0_No < x1 & x1 in X & y1 in Y ) and
A3: z = (1_No + ((x1 - x) * y1)) * (x1 ") by Def15;
A4: (1_No + ((x1 - y) * y1)) * (x1 ") in divset (X,y,Y) by A2, Def15;
- x == - y by A1, SURREALR:10;
then x1 + (- x) == x1 + (- y) by SURREALR:43;
then (x1 + (- x)) * y1 == (x1 + (- y)) * y1 by SURREALR:51;
then 1_No + ((x1 + (- x)) * y1) == 1_No + ((x1 + (- y)) * y1) by SURREALR:43;
then z == (1_No + ((x1 + (- y)) * y1)) * (x1 ") by A3, SURREALR:51;
hence ex b₁, b₂ being set st
( b₁ in divset (X,y,Y) & b₂ in divset (X,y,Y) & b₁ <= z & z <= b₂ ) by A4; :: thesis:

end;

theorem Th36: :: SURREALI:36

for x being Surreal st x is positive holds
x " = [(({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x "))))),((divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x ")))))]

end;

theorem Th37: :: SURREALI:37

for X1, X2, Y1, Y2 being surreal-membered set st X2 <=_ X1 & Y2 <=_ Y1 & [X1,Y1] is surreal holds
[X2,Y2] is surreal

let X1, X2, Y1, Y2 be surreal-membered set ; :: thesis:
assume A1: ( X2 <=_ X1 & Y2 <=_ Y1 & [X1,Y1] is surreal ) ; :: thesis:
A2: X2 << Y2

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A3: ( l in X2 & r in Y2 ) ; :: thesis:
consider l1, l2 being Surreal such that
A4: ( l1 in X1 & l2 in X1 & l1 <= l & l <= l2 ) by A3, A1;
consider r1, r2 being Surreal such that
A5: ( r1 in Y1 & r2 in Y1 & r1 <= r & r <= r2 ) by A3, A1;
( X1 = L_ [X1,Y1] & L_ [X1,Y1] << R_ [X1,Y1] & R_ [X1,Y1] = Y1 ) by A1, SURREAL0:45;
then l < r1 by A4, A5, SURREALO:4;
hence not r <= l by A5, SURREALO:4; :: thesis:

end;

consider M being Ordinal such that
A6: for o being object st o in X2 \/ Y2 holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
[X2,Y2] in Day M by A6, A2, SURREAL0:46;
hence [X2,Y2] is surreal ; :: thesis:

end;

theorem :: SURREALI:38

for x being Surreal st x is positive holds
[(({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x "))))),((divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))))] is Surreal

let x be Surreal; :: thesis:
set Nx = ||.x.||;
assume A1: x is positive ; :: thesis:
then divset ((R_ x),x,(L_ (x "))) <=_ divset ((R_ x),||.x.||,(L_ (x "))) by Th18, Th35;
then A2: {0_No} \/ (divset ((R_ x),x,(L_ (x ")))) <=_ {0_No} \/ (divset ((R_ x),||.x.||,(L_ (x ")))) by SURREALO:31;
divset ((L_ x),x,(R_ (x "))) <=_ divset ((L_ x),||.x.||,(R_ (x "))) by A1, Th18, Th35;
then A3: ({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x ")))) <=_ ({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x ")))) by A2, SURREALO:31;
( divset ((L_ x),x,(L_ (x "))) <=_ divset ((L_ x),||.x.||,(L_ (x "))) & divset ((R_ x),x,(R_ (x "))) <=_ divset ((R_ x),||.x.||,(R_ (x "))) ) by A1, Th18, Th35;
then A4: (divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))) <=_ (divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x ")))) by SURREALO:31;
[(({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x "))))),((divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x ")))))] is Surreal by A1, Th36;
hence [(({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x "))))),((divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))))] is Surreal by TARSKI:1, Th37, A3, A4; :: thesis:

end;

theorem :: SURREALI:39

for x, y being Surreal st x is positive & y = [(({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x "))))),((divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))))] holds
x " == y

let x, y be Surreal; :: thesis:
set Nx = ||.x.||;
assume A1: x is positive ; :: thesis:
then A2: x == ||.x.|| by Th18;
then divset ((R_ x),x,(L_ (x "))) <==> divset ((R_ x),||.x.||,(L_ (x "))) by Th35;
then A3: {0_No} \/ (divset ((R_ x),x,(L_ (x ")))) <==> {0_No} \/ (divset ((R_ x),||.x.||,(L_ (x ")))) by SURREALO:31;
divset ((L_ x),x,(R_ (x "))) <==> divset ((L_ x),||.x.||,(R_ (x "))) by A2, Th35;
then A4: ({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x ")))) <==> ({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x ")))) by A3, SURREALO:31;
( divset ((L_ x),x,(L_ (x "))) <==> divset ((L_ x),||.x.||,(L_ (x "))) & divset ((R_ x),x,(R_ (x "))) <==> divset ((R_ x),||.x.||,(R_ (x "))) ) by A2, Th35;
then A5: (divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))) <==> (divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x ")))) by SURREALO:31;
assume A6: y = [(({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x "))))),((divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))))] ; :: thesis:
x " = [(({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x "))))),((divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x ")))))] by A1, Th36;
hence x " == y by SURREALO:29, A6, A4, A5; :: thesis:

end;

theorem Th40: :: SURREALI:40

for x being Surreal st not x == 0_No holds
( 0_No < x iff 0_No < x " )

let x be Surreal; :: thesis:
assume not x == 0_No ; :: thesis:
then A1: x * (x ") == 1_No by Th33;
A2: 0_No < x * (x ") by A1, SURREALO:4, Def8;
thus ( 0_No < x implies 0_No < x " ) :: thesis:

assume 0_No < x ; :: thesis:
then 0_No <= x ;
hence 0_No < x " by A2, SURREALR:72; :: thesis:

end;

assume 0_No < x " ; :: thesis:
then 0_No <= x " ;
hence 0_No < x by A2, SURREALR:72; :: thesis:

end;

registration

let x be positive Surreal;

cluster x " -> positive ;

not 0_No == x by Def8;
hence x " is positive by Def8, Th40; :: thesis:

end;

theorem Lm3: :: SURREALI:41

for x, y being Surreal holds
( x * y == 0_No iff ( x == 0_No or y == 0_No ) ) by SURREALR:72, SURREALR:74;

theorem Th41: :: SURREALI:42

for x, y being Surreal st not x == 0_No & x * y == 1_No holds
y == x "

let x, y be Surreal; :: thesis:
assume A1: ( not x == 0_No & x * y == 1_No ) ; :: thesis:
then A2: x * (x ") == 1_No by Th33;
( ((x ") * x) * y == (x ") * (x * y) & (x ") * (x * y) == 1_No * (x ") ) by A1, SURREALR:54, SURREALR:69;
then ( 1_No * y == ((x ") * x) * y & ((x ") * x) * y == x " ) by A2, SURREALR:54, SURREALO:4;
hence y == x " by SURREALO:4; :: thesis:

end;

theorem :: SURREALI:43

for x, y being Surreal st not 0_No == x & x == y holds
x " == y "

let x, y be Surreal; :: thesis:
assume A1: ( not 0_No == x & x == y ) ; :: thesis:
then A2: not 0_No == y by SURREALO:4;
( y * (x ") == x * (x ") & x * (x ") == 1_No ) by A1, Th33, SURREALR:54;
then y * (x ") == 1_No by SURREALO:4;
hence x " == y " by A2, Th41; :: thesis:

end;

theorem :: SURREALI:44

for x being Surreal st not x == 0_No holds
(x ") " == x

let x be Surreal; :: thesis:
assume not x == 0_No ; :: thesis:
then A1: ( 0_No < 1_No & 1_No == x * (x ") ) by Th33, Def8;
then not x * (x ") == 0_No by SURREALO:4;
then not x " == 0_No by SURREALR:72, SURREALR:74;
hence (x ") " == x by A1, Th41; :: thesis:

end;

theorem :: SURREALI:45

for x, y being Surreal st not x == 0_No & not y == 0_No holds
(x * y) " == (x ") * (y ")