let r be Sequence of REAL ; :: thesis: for y being positive decreasing_infinitely Surreal-Sequence ex s being uSurreal-Sequence st
( dom s = succ ((dom r) /\ (dom y)) & s,y,r simplest_up_to dom s )
let y be positive decreasing_infinitely Surreal-Sequence; :: thesis: ex s being uSurreal-Sequence st
( dom s = succ ((dom r) /\ (dom y)) & s,y,r simplest_up_to dom s )
defpred S₁[ Ordinal] means ( $1 c= (dom r) /\ (dom y) implies ex s being uSurreal-Sequence st
( dom s = succ $1 & s,y,r simplest_up_to dom s ) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
assume A3: D c= (dom r) /\ (dom y) ; :: thesis: ex s being uSurreal-Sequence st
( dom s = succ D & s,y,r simplest_up_to dom s )
then A4: ( D c= dom y & D c= dom r ) by XBOOLE_1:18;
A5: ( D c= dom y & D c= dom r ) by A3, XBOOLE_1:18;

per cases ( D = {} or ( D is limit_ordinal & D <> {} ) or not D is limit_ordinal ) ;

suppose A6: D = {} ; :: thesis: ex s being uSurreal-Sequence st
( dom s = succ D & s,y,r simplest_up_to dom s )

take s = <%0_No%>; :: thesis: ( dom s = succ D & s,y,r simplest_up_to dom s )
thus A7: dom s = succ D by A6, AFINSQ_1:def 4; :: thesis: s,y,r simplest_up_to dom s
let A be Ordinal; :: according to SURREALC:def 19 :: thesis: ( A in dom s implies s,y,r simplest_on_position A )
assume A8: A in dom s ; :: thesis: s,y,r simplest_on_position A
let sa be Surreal; :: according to SURREALC:def 18 :: thesis: ( sa = s . A implies ( ( 0 = A implies sa = 0_No ) & ( 0 <> A implies ( sa in_meets_terms s,y,r,A & ( for x being uSurreal st x in_meets_terms s,y,r,A & x <> sa holds
born sa in born x ) ) ) ) )
assume sa = s . A ; :: thesis: ( ( 0 = A implies sa = 0_No ) & ( 0 <> A implies ( sa in_meets_terms s,y,r,A & ( for x being uSurreal st x in_meets_terms s,y,r,A & x <> sa holds
born sa in born x ) ) ) )
hence ( ( 0 = A implies sa = 0_No ) & ( 0 <> A implies ( sa in_meets_terms s,y,r,A & ( for x being uSurreal st x in_meets_terms s,y,r,A & x <> sa holds
born sa in born x ) ) ) ) by A8, A6, A7, ORDINAL1:8; :: thesis: verum

end;

suppose A9: ( D is limit_ordinal & D <> {} ) ; :: thesis: ex s being uSurreal-Sequence st
( dom s = succ D & s,y,r simplest_up_to dom s )

defpred S₂[ object , object ] means for A being Ordinal st A = $1 holds
( $2 is uSurreal-Sequence & ( for s being uSurreal-Sequence st s = $2 holds
( dom s = succ A & s,y,r simplest_up_to dom s ) ) );
A10: for e being object st e in D holds
ex o being object st S₂[e,o]

proof

let e be object ; :: thesis: ( e in D implies ex o being object st S₂[e,o] )
assume A11: e in D ; :: thesis: ex o being object st S₂[e,o]
reconsider E = e as Ordinal by A11;
consider s being uSurreal-Sequence such that
A12: ( dom s = succ E & s,y,r simplest_up_to dom s ) by A11, ORDINAL1:def 2, A3, A2;
take s ; :: thesis: S₂[e,s]
thus S₂[e,s] by A12; :: thesis: verum

end;

consider S being Function such that
A13: ( dom S = D & ( for o being object st o in D holds
S₂[o,S . o] ) ) from CLASSES1:sch 1(A10);
for o being object st o in rng S holds
o is Function

proof

let o be object ; :: thesis: ( o in rng S implies o is Function )
assume o in rng S ; :: thesis: o is Function
then ex a being object st
( a in dom S & S . a = o ) by FUNCT_1:def 3;
hence o is Function by A13; :: thesis: verum

end;

then S is Function-yielding by FUNCT_1:def 13;
then reconsider S = S as Function-yielding Function ;
deffunc H₁( Ordinal) -> set = (S . $1) . $1;
consider s being Sequence such that
A14: ( dom s = D & ( for A being Ordinal st A in D holds
s . A = H₁(A) ) ) from ORDINAL2:sch 2();
rng s is uniq-surreal-membered

proof

let a be object ; :: according to SURREALO:def 12 :: thesis: ( not a in rng s or a is set )
assume A15: a in rng s ; :: thesis: a is set
consider x being object such that
A16: ( x in dom s & s . x = a ) by A15, FUNCT_1:def 3;
reconsider x = x as Ordinal by A16;
reconsider Sx = S . x as uSurreal-Sequence by A16, A13, A14;
( x in succ x & succ x = dom Sx ) by A16, A14, A13, ORDINAL1:6;
then Sx . x in rng Sx by FUNCT_1:def 3;
then Sx . x is uSurreal by SURREALO:def 12;
hence a is set by A14, A16; :: thesis: verum

end;

then reconsider s = s as uSurreal-Sequence by Def10;
defpred S₃[ Ordinal] means ( $1 in D implies ( S . $1 = s | (succ $1) & s,y,r simplest_on_position $1 ) );
A17: for E being Ordinal holds S₃[E]

proof

let E be Ordinal; :: thesis: S₃[E]
assume A18: E in D ; :: thesis: ( S . E = s | (succ E) & s,y,r simplest_on_position E )
reconsider SE = S . E as uSurreal-Sequence by A18, A13;
A19: succ E c= D by ORDINAL1:def 2, A18, A9, ORDINAL1:28;
A20: ( dom SE = succ E & SE,y,r simplest_up_to dom SE ) by A18, A13;
A21: dom (s | (succ E)) = succ E by A19, RELAT_1:62, A14;
for o being object st o in succ E holds
(s | (succ E)) . o = SE . o

proof

let o be object ; :: thesis: ( o in succ E implies (s | (succ E)) . o = SE . o )
assume A22: o in succ E ; :: thesis: (s | (succ E)) . o = SE . o
then reconsider o = o as Ordinal ;
A23: (s | (succ E)) . o = s . o by A22, FUNCT_1:49;

per cases ( o in E or o = E ) by A22, ORDINAL1:8;

suppose A24: o in E ; :: thesis: (s | (succ E)) . o = SE . o

A25: o in D by A18, A24, ORDINAL1:10;
reconsider So = S . o as uSurreal-Sequence by A25, A13;
A26: So . o = s . o by A14, A18, A24, ORDINAL1:10;
A27: ( dom So = succ o & So,y,r simplest_up_to dom So ) by A25, A13;
A28: dom So c= dom SE by A27, A20, A22, ORDINAL1:21;
A29: SE,y,r simplest_up_to dom So by A28, A20;
( (So | (succ o)) . o = So . o & (SE | (succ o)) . o = SE . o ) by ORDINAL1:6, FUNCT_1:49;
hence (s | (succ E)) . o = SE . o by A26, A23, A27, A29, A28, Th78; :: thesis: verum

end;

suppose o = E ; :: thesis: (s | (succ E)) . o = SE . o

hence (s | (succ E)) . o = SE . o by A23, A14, A18; :: thesis: verum

end;

end;

end;

then A30: s | (succ E) = SE by A20, A21, FUNCT_1:2;
E in succ E by ORDINAL1:6;
hence ( S . E = s | (succ E) & s,y,r simplest_on_position E ) by A20, A30, Th81; :: thesis: verum

end;

then A31: s,y,r simplest_up_to D ;
defpred S₄[ object , object ] means ( $2 is Surreal & ( for A being Ordinal st A = $1 holds
for sa, ya being Surreal st sa = s . (succ A) & ya = y . (succ A) holds
$2 = (sa + ((uReal . (r . (succ A))) * ya)) + ya ) );
A32: for e being object st e in D holds
ex o being object st S₄[e,o]

proof

let e be object ; :: thesis: ( e in D implies ex o being object st S₄[e,o] )
assume A33: e in D ; :: thesis: ex o being object st S₄[e,o]
reconsider E = e as Ordinal by A33;
succ E in D by A33, A9, ORDINAL1:28;
then ( y . (succ E) in rng y & s . (succ E) in rng s ) by A4, A14, FUNCT_1:def 3;
then reconsider ya = y . (succ E), sa = s . (succ E) as Surreal by SURREAL0:def 16;
take o = (sa + ((uReal . (r . (succ E))) * ya)) + ya; :: thesis: S₄[e,o]
thus S₄[e,o] ; :: thesis: verum

end;

consider upp being Function such that
A34: dom upp = D and
A35: for o being object st o in D holds
S₄[o,upp . o] from CLASSES1:sch 1(A32);
A36: rng upp is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in rng upp or o is surreal )
assume A37: o in rng upp ; :: thesis: o is surreal
ex a being object st
( a in dom upp & upp . a = o ) by A37, FUNCT_1:def 3;
hence o is surreal by A34, A35; :: thesis: verum

end;

A38: for A, B being Ordinal st A in B & B in D holds
for uA, uB being Surreal st uA = upp . A & uB = upp . B holds
uB < uA

proof

let A, B be Ordinal; :: thesis: ( A in B & B in D implies for uA, uB being Surreal st uA = upp . A & uB = upp . B holds
uB < uA )
assume A39: ( A in B & B in D ) ; :: thesis: for uA, uB being Surreal st uA = upp . A & uB = upp . B holds
uB < uA
let uA, uB be Surreal; :: thesis: ( uA = upp . A & uB = upp . B implies uB < uA )
assume A40: ( uA = upp . A & uB = upp . B ) ; :: thesis: uB < uA
A41: succ B in D by A39, A9, ORDINAL1:28;
then ( y . (succ B) in rng y & s . (succ B) in rng s ) by A4, A14, FUNCT_1:def 3;
then reconsider yB = y . (succ B), sB = s . (succ B) as Surreal by SURREAL0:def 16;
reconsider NB = yB as positive Surreal by A4, Def15, A41;
A42: A in D by A39, ORDINAL1:10;
then A43: succ A in D by A9, ORDINAL1:28;
then ( y . (succ A) in rng y & s . (succ A) in rng s ) by A4, A14, FUNCT_1:def 3;
then reconsider yA = y . (succ A), sA = s . (succ A) as Surreal by SURREAL0:def 16;
reconsider NA = yA as positive Surreal by A4, Def15, A43;
A44: succ B in D by A39, A9, ORDINAL1:28;
s,y,r simplest_on_position succ B by A31, A39, A9, ORDINAL1:28;
then A45: sB in_meets_terms s,y,r, succ B ;
set n = 2;
A46: ( uA = (sA + ((uReal . (r . (succ A))) * NA)) + NA & uB = (sB + ((uReal . (r . (succ B))) * NB)) + NB ) by A40, A42, A39, A35;
A47: succ A c= B by A39, ORDINAL1:21;
then sB is sA,yA,r . (succ A) _Term by A45, ORDINAL1:22;
then |.(sB + (- (sA + ((uReal . (r . (succ A))) * NA)))).| infinitely< NA * (uReal . (1 / 2)) by Th13;
then |.(sB + (- (sA + ((uReal . (r . (succ A))) * NA)))).| < NA * (uReal . (1 / 2)) by Th9;
then sB - (sA + ((uReal . (r . (succ A))) * NA)) < NA * (uReal . (1 / 2)) by Th52;
then A48: sB < (NA * (uReal . (1 / 2))) + (sA + ((uReal . (r . (succ A))) * NA)) by SURREALR:41;
((uReal . (r . (succ B))) * NB) + NB = ((uReal . (r . (succ B))) * NB) + ((uReal . 1) * NB) by SURREALN:48;
then A49: ((uReal . (r . (succ B))) * NB) + NB == ((uReal . (r . (succ B))) + (uReal . 1)) * NB by SURREALR:67;
((uReal . (r . (succ B))) + (uReal . 1)) * NB == (uReal . (1 + (r . (succ B)))) * NB by SURREALR:51, SURREALN:55;
then A50: ((uReal . (r . (succ B))) * NB) + NB == (uReal . (1 + (r . (succ B)))) * NB by A49, SURREALO:4;
NB infinitely< NA by A4, Def16, A47, ORDINAL1:22, A44;
then ( 0_No <= NB & NB infinitely< NA * (uReal . (1 / 2)) ) by Th13, SURREALI:def 8;
then (uReal . (1 + (r . (succ B)))) * NB < NA * (uReal . (1 / 2)) by Th20;
then A51: ((uReal . (r . (succ B))) * NB) + NB < NA * (uReal . (1 / 2)) by A50, SURREALO:4;
uB = sB + (((uReal . (r . (succ B))) * NB) + NB) by A46, SURREALR:37;
then A52: uB <= sB + (NA * (uReal . (1 / 2))) by A51, SURREALR:44;
sB + (NA * (uReal . (1 / 2))) < ((NA * (uReal . (1 / 2))) + (sA + ((uReal . (r . (succ A))) * NA))) + (NA * (uReal . (1 / 2))) by A48, SURREALR:44;
then A53: uB < ((NA * (uReal . (1 / 2))) + (sA + ((uReal . (r . (succ A))) * NA))) + (NA * (uReal . (1 / 2))) by A52, SURREALO:4;
(1 / 2) + (1 / 2) = 1 ;
then A54: ( NA * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == NA * 1_No & NA * 1_No = NA ) by SURREALR:51, SURREALN:55, SURREALN:48;
NA * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == (NA * (uReal . (1 / 2))) + (NA * (uReal . (1 / 2))) by SURREALR:67;
then A55: NA == (NA * (uReal . (1 / 2))) + (NA * (uReal . (1 / 2))) by A54, SURREALO:4;
( ((NA * (uReal . (1 / 2))) + (sA + ((uReal . (r . (succ A))) * NA))) + (NA * (uReal . (1 / 2))) = ((NA * (uReal . (1 / 2))) + (NA * (uReal . (1 / 2)))) + (sA + ((uReal . (r . (succ A))) * NA)) & ((NA * (uReal . (1 / 2))) + (NA * (uReal . (1 / 2)))) + (sA + ((uReal . (r . (succ A))) * NA)) == NA + (sA + ((uReal . (r . (succ A))) * NA)) ) by SURREALR:37, A55, SURREALR:43;
hence uB < uA by A46, A53, SURREALO:4; :: thesis: verum

end;

defpred S₅[ object , object ] means ( $2 is Surreal & ( for A being Ordinal st A = $1 holds
for sa, ya being Surreal st sa = s . (succ A) & ya = y . (succ A) holds
$2 = (sa + ((uReal . (r . (succ A))) * ya)) + (- ya) ) );
A56: for e being object st e in D holds
ex o being object st S₅[e,o]

proof

let e be object ; :: thesis: ( e in D implies ex o being object st S₅[e,o] )
assume A57: e in D ; :: thesis: ex o being object st S₅[e,o]
reconsider E = e as Ordinal by A57;
succ E in D by A57, A9, ORDINAL1:28;
then ( y . (succ E) in rng y & s . (succ E) in rng s ) by A4, A14, FUNCT_1:def 3;
then reconsider ya = y . (succ E), sa = s . (succ E) as Surreal by SURREAL0:def 16;
take o = (sa + ((uReal . (r . (succ E))) * ya)) + (- ya); :: thesis: S₅[e,o]
thus S₅[e,o] ; :: thesis: verum

end;

consider low being Function such that
A58: dom low = D and
A59: for o being object st o in D holds
S₅[o,low . o] from CLASSES1:sch 1(A56);
A60: rng low is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in rng low or o is surreal )
assume A61: o in rng low ; :: thesis: o is surreal
ex a being object st
( a in dom low & low . a = o ) by A61, FUNCT_1:def 3;
hence o is surreal by A58, A59; :: thesis: verum

end;

A62: for A, B being Ordinal st A in B & B in D holds
for lA, lB being Surreal st lA = low . A & lB = low . B holds
lA < lB

proof

let A, B be Ordinal; :: thesis: ( A in B & B in D implies for lA, lB being Surreal st lA = low . A & lB = low . B holds
lA < lB )
assume A63: ( A in B & B in D ) ; :: thesis: for lA, lB being Surreal st lA = low . A & lB = low . B holds
lA < lB
let uA, uB be Surreal; :: thesis: ( uA = low . A & uB = low . B implies uA < uB )
assume A64: ( uA = low . A & uB = low . B ) ; :: thesis: uA < uB
A65: ( succ B in D & D c= dom y ) by A3, XBOOLE_1:18, A63, A9, ORDINAL1:28;
( y . (succ B) in rng y & s . (succ B) in rng s ) by A65, A14, FUNCT_1:def 3;
then reconsider yB = y . (succ B), sB = s . (succ B) as Surreal by SURREAL0:def 16;
reconsider NB = yB as positive Surreal by A65, Def15;
A66: A in D by A63, ORDINAL1:10;
then A67: succ A in D by A9, ORDINAL1:28;
then ( y . (succ A) in rng y & s . (succ A) in rng s ) by A4, A14, FUNCT_1:def 3;
then reconsider yA = y . (succ A), sA = s . (succ A) as Surreal by SURREAL0:def 16;
reconsider NA = yA as positive Surreal by A67, A65, Def15;
A68: succ B in D by A63, A9, ORDINAL1:28;
s,y,r simplest_on_position succ B by A31, A63, A9, ORDINAL1:28;
then A69: sB in_meets_terms s,y,r, succ B ;
set n = 2;
A70: ( uA = (sA + ((uReal . (r . (succ A))) * NA)) + (- NA) & uB = (sB + ((uReal . (r . (succ B))) * NB)) + (- NB) ) by A64, A66, A63, A59;
A71: succ A c= B by A63, ORDINAL1:21;
then sB is sA,yA,r . (succ A) _Term by A69, ORDINAL1:22;
then |.(sB + (- (sA + ((uReal . (r . (succ A))) * NA)))).| infinitely< NA * (uReal . (1 / 2)) by Th13;
then |.(sB + (- (sA + ((uReal . (r . (succ A))) * NA)))).| < NA * (uReal . (1 / 2)) by Th9;
then - (NA * (uReal . (1 / 2))) < sB - (sA + ((uReal . (r . (succ A))) * NA)) by Th52;
then A72: (- (NA * (uReal . (1 / 2)))) + (sA + ((uReal . (r . (succ A))) * NA)) < sB by SURREALR:42;
(- ((uReal . (r . (succ B))) * NB)) + NB = ((- (uReal . (r . (succ B)))) * NB) + ((uReal . 1) * NB) by SURREALR:58, SURREALN:48;
then A73: (- ((uReal . (r . (succ B))) * NB)) + NB == ((- (uReal . (r . (succ B)))) + (uReal . 1)) * NB by SURREALR:67;
- (uReal . (r . (succ B))) == uReal . (- (r . (succ B))) by SURREALN:56;
then A74: (- (uReal . (r . (succ B)))) + (uReal . 1) == (uReal . (- (r . (succ B)))) + (uReal . 1) by SURREALR:43;
(uReal . (- (r . (succ B)))) + (uReal . 1) == uReal . (1 + (- (r . (succ B)))) by SURREALN:55;
then (- (uReal . (r . (succ B)))) + (uReal . 1) == uReal . (1 + (- (r . (succ B)))) by A74, SURREALO:4;
then ((- (uReal . (r . (succ B)))) + (uReal . 1)) * NB == (uReal . (1 + (- (r . (succ B))))) * NB by SURREALR:51;
then A75: (- ((uReal . (r . (succ B))) * NB)) + NB == (uReal . (1 + (- (r . (succ B))))) * NB by A73, SURREALO:4;
NB infinitely< NA by A4, Def16, A71, ORDINAL1:22, A68;
then ( 0_No <= NB & NB infinitely< NA * (uReal . (1 / 2)) ) by Th13, SURREALI:def 8;
then (uReal . (1 + (- (r . (succ B))))) * NB < NA * (uReal . (1 / 2)) by Th20;
then (- ((uReal . (r . (succ B))) * NB)) + NB < NA * (uReal . (1 / 2)) by A75, SURREALO:4;
then A76: ( - (NA * (uReal . (1 / 2))) < - ((- ((uReal . (r . (succ B))) * NB)) + NB) & - ((- ((uReal . (r . (succ B))) * NB)) + NB) = (- (- ((uReal . (r . (succ B))) * NB))) + (- NB) ) by SURREALR:10, SURREALR:40;
sB + (((uReal . (r . (succ B))) * NB) + (- NB)) = uB by A70, SURREALR:37;
then A77: sB + (- (NA * (uReal . (1 / 2)))) < uB by A76, SURREALR:44;
((- (NA * (uReal . (1 / 2)))) + (sA + ((uReal . (r . (succ A))) * NA))) + (- (NA * (uReal . (1 / 2)))) <= sB + (- (NA * (uReal . (1 / 2)))) by A72, SURREALR:44;
then A78: ((- (NA * (uReal . (1 / 2)))) + (sA + ((uReal . (r . (succ A))) * NA))) + (- (NA * (uReal . (1 / 2)))) < uB by A77, SURREALO:4;
(1 / 2) + (1 / 2) = 1 ;
then A79: ( NA * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == NA * 1_No & NA * 1_No = NA ) by SURREALN:55, SURREALN:48, SURREALR:51;
NA * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == (NA * (uReal . (1 / 2))) + (NA * (uReal . (1 / 2))) by SURREALR:67;
then NA == (NA * (uReal . (1 / 2))) + (NA * (uReal . (1 / 2))) by A79, SURREALO:4;
then - NA == - ((NA * (uReal . (1 / 2))) + (NA * (uReal . (1 / 2)))) by SURREALR:10;
then A80: - NA == (- (NA * (uReal . (1 / 2)))) + (- (NA * (uReal . (1 / 2)))) by SURREALR:40;
( ((- (NA * (uReal . (1 / 2)))) + (sA + ((uReal . (r . (succ A))) * NA))) + (- (NA * (uReal . (1 / 2)))) = ((- (NA * (uReal . (1 / 2)))) + (- (NA * (uReal . (1 / 2))))) + (sA + ((uReal . (r . (succ A))) * NA)) & ((- (NA * (uReal . (1 / 2)))) + (- (NA * (uReal . (1 / 2))))) + (sA + ((uReal . (r . (succ A))) * NA)) == (- NA) + (sA + ((uReal . (r . (succ A))) * NA)) ) by SURREALR:37, A80, SURREALR:43;
hence uA < uB by A78, A70, SURREALO:4; :: thesis: verum

end;

A81: for A being Ordinal st A in D holds
for lA, uA being Surreal st lA = low . A & uA = upp . A holds
lA < uA

proof

let A be Ordinal; :: thesis: ( A in D implies for lA, uA being Surreal st lA = low . A & uA = upp . A holds
lA < uA )
assume A82: A in D ; :: thesis: for lA, uA being Surreal st lA = low . A & uA = upp . A holds
lA < uA
let lA, uA be Surreal; :: thesis: ( lA = low . A & uA = upp . A implies lA < uA )
assume A83: ( lA = low . A & uA = upp . A ) ; :: thesis: lA < uA
A84: succ A in D by A82, A9, ORDINAL1:28;
then ( y . (succ A) in rng y & s . (succ A) in rng s ) by A4, A14, FUNCT_1:def 3;
then reconsider yA = y . (succ A), sA = s . (succ A) as Surreal by SURREAL0:def 16;
reconsider NA = yA as positive Surreal by A84, A4, Def15;
A85: ( lA = (sA + ((uReal . (r . (succ A))) * NA)) + (- NA) & uA = (sA + ((uReal . (r . (succ A))) * NA)) + NA ) by A82, A83, A59, A35;
( - NA <= - 0_No & - 0_No = 0_No ) by SURREALI:def 8, SURREALR:10;
then - NA < NA by SURREALI:def 8, SURREALO:4;
hence lA < uA by A85, SURREALR:44; :: thesis: verum

end;

A86: rng low << rng upp

proof

let l, u be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in rng low or not u in rng upp or not u <= l )
assume A87: ( l in rng low & u in rng upp ) ; :: thesis: not u <= l
consider A being object such that
A88: ( A in dom low & low . A = l ) by A87, FUNCT_1:def 3;
consider B being object such that
A89: ( B in dom upp & upp . B = u ) by A87, FUNCT_1:def 3;
reconsider A = A, B = B as Ordinal by A88, A89, A58, A34;
reconsider lowB = low . B, uppA = upp . A as Surreal by A88, A89, A58, A59, A34, A35;

per cases ( A = B or A in B or B in A ) by ORDINAL1:14;

suppose A = B ; :: thesis: not u <= l

hence not u <= l by A88, A89, A81, A58; :: thesis: verum

end;

suppose A in B ; :: thesis: not u <= l

then ( l < lowB & lowB <= u ) by A62, A88, A89, A34, A81;
hence not u <= l by SURREALO:4; :: thesis: verum

end;

suppose B in A ; :: thesis: not u <= l

then ( l <= uppA & uppA < u ) by A38, A88, A89, A58, A81;
hence not u <= l by SURREALO:4; :: thesis: verum

end;

end;

end;

consider M being Ordinal such that
A90: for o being object st o in (rng low) \/ (rng upp) holds
ex A being Ordinal st
( A in M & o in Day A ) by A36, A60, SURREAL0:47;
[(rng low),(rng upp)] in Day M by A86, A90, SURREAL0:46;
then reconsider rLU = [(rng low),(rng upp)] as Surreal ;
defpred S₆[ Surreal] means $1 in_meets_terms s,y,r,D;
rLU in_meets_terms s,y,r,D

proof

let A be Ordinal; :: according to SURREALC:def 17 :: thesis: for sb, yb being Surreal st A in D & sb = s . A & yb = y . A holds
rLU is sb,yb,r . A _Term
let sb, yb be Surreal; :: thesis: ( A in D & sb = s . A & yb = y . A implies rLU is sb,yb,r . A _Term )
assume A91: ( A in D & sb = s . A & yb = y . A ) ; :: thesis: rLU is sb,yb,r . A _Term
reconsider lowA = low . A, uppA = upp . A as Surreal by A91, A59, A35;
A92: succ A in D by A91, A9, ORDINAL1:28;
then ( y . (succ A) in rng y & s . (succ A) in rng s ) by A4, A14, FUNCT_1:def 3;
then reconsider yA = y . (succ A), sA = s . (succ A) as Surreal by SURREAL0:def 16;
reconsider NA = yA, NB = yb as positive Surreal by A91, A92, A4, Def15;
A93: ( lowA = (sA + ((uReal . (r . (succ A))) * NA)) + (- NA) & uppA = (sA + ((uReal . (r . (succ A))) * NA)) + NA ) by A91, A59, A35;
s,y,r simplest_on_position succ A by A31, A91, A9, ORDINAL1:28;
then A94: sA in_meets_terms s,y,r, succ A ;
A95: sA is sb,yb,r . A _Term by ORDINAL1:6, A91, A94;
A96: NA infinitely< NB by Def16, ORDINAL1:6, A92, A91, A5;
A97: ( lowA in rng low & uppA in rng upp ) by A91, A58, A34, FUNCT_1:def 3;
A98: ( L_ rLU << {rLU} & {rLU} << R_ rLU & rLU in {rLU} ) by SURREALO:11, TARSKI:def 1;
then - rLU < - ((sA + ((uReal . (r . (succ A))) * NA)) + (- NA)) by A97, A93, SURREALR:10;
then A99: (- rLU) + (sb + ((uReal . (r . A)) * NB)) <= (- ((sA + ((uReal . (r . (succ A))) * NA)) + (- NA))) + (sb + ((uReal . (r . A)) * NB)) by SURREALR:44;
A100: (- rLU) + (sb + ((uReal . (r . A)) * NB)) = (- rLU) + (- (- (sb + ((uReal . (r . A)) * NB))))
.= - (rLU + (- (sb + ((uReal . (r . A)) * NB)))) by SURREALR:40 ;
A101: (- ((sA + ((uReal . (r . (succ A))) * NA)) + (- NA))) + (sb + ((uReal . (r . A)) * NB)) = ((- (sA + ((uReal . (r . (succ A))) * NA))) + (- (- NA))) + (sb + ((uReal . (r . A)) * NB)) by SURREALR:40
.= (((- sA) + (- ((uReal . (r . (succ A))) * NA))) + NA) + (sb + ((uReal . (r . A)) * NB)) by SURREALR:40
.= ((- sA) + ((- ((uReal . (r . (succ A))) * NA)) + NA)) + (sb + ((uReal . (r . A)) * NB)) by SURREALR:37
.= ((- sA) + (- (- (sb + ((uReal . (r . A)) * NB))))) + ((- ((uReal . (r . (succ A))) * NA)) + NA) by SURREALR:37
.= (- (sA + (- (sb + ((uReal . (r . A)) * NB))))) + ((- ((uReal . (r . (succ A))) * NA)) + NA) by SURREALR:40 ;
A102: 0_No <= NA by SURREALI:def 8;
then A103: NA = |.NA.| by Def6;
A104: |.((uReal . (r . (succ A))) * NA).| infinitely< NB by A96, A102, Th53;
then |.(NA + ((uReal . (r . (succ A))) * NA)).| infinitely< NB by A96, Th41, A103;
then A105: |.((sA + (- (sb + ((uReal . (r . A)) * NB)))) + (NA + ((uReal . (r . (succ A))) * NA))).| infinitely< NB by A95, Th41;
A106: |.(- (sA + (- (sb + ((uReal . (r . A)) * NB))))).| infinitely< NB by A95, Th42;
|.(NA - ((uReal . (r . (succ A))) * NA)).| infinitely< NB by A96, Th43, A103, A104;
then A107: |.((- (sA + (- (sb + ((uReal . (r . A)) * NB))))) + (NA + (- ((uReal . (r . (succ A))) * NA)))).| infinitely< NB by A106, Th41;
(- (sA + (- (sb + ((uReal . (r . A)) * NB))))) + (NA + (- ((uReal . (r . (succ A))) * NA))) infinitely< NB by Th34, Th11, A107;
then A108: - (rLU + (- (sb + ((uReal . (r . A)) * NB)))) infinitely< NB by A100, A99, A101, Th11;
A109: rLU + (- (sb + ((uReal . (r . A)) * NB))) <= ((sA + ((uReal . (r . (succ A))) * NA)) + NA) + (- (sb + ((uReal . (r . A)) * NB))) by A97, A98, A93, SURREALR:44;
A110: ((sA + ((uReal . (r . (succ A))) * NA)) + NA) + (- (sb + ((uReal . (r . A)) * NB))) = (sA + (((uReal . (r . (succ A))) * NA) + NA)) + (- (sb + ((uReal . (r . A)) * NB))) by SURREALR:37
.= (sA + (- (sb + ((uReal . (r . A)) * NB)))) + (NA + ((uReal . (r . (succ A))) * NA)) by SURREALR:37 ;
(sA + (- (sb + ((uReal . (r . A)) * NB)))) + (NA + ((uReal . (r . (succ A))) * NA)) infinitely< NB by Th34, A105, Th11;
then rLU + (- (sb + ((uReal . (r . A)) * NB))) infinitely< NB by A110, A109, Th11;
hence rLU is sb,yb,r . A _Term by Def6, A108; :: thesis: verum

end;

then A111: ex x being Surreal st S₆[x] ;
A112: for x, y, z being Surreal st x <= y & y <= z & S₆[x] & S₆[z] holds
S₆[y] by Th82, A3, XBOOLE_1:18;
consider sD being uSurreal such that
A113: S₆[sD] and
A114: for x being uSurreal st S₆[x] & x <> sD holds
born sD in born x from SURREALC:sch 1(A111, A112);
take ssD = s ^ <%sD%>; :: thesis: ( dom ssD = succ D & ssD,y,r simplest_up_to dom ssD )
A115: dom <%sD%> = 1 by AFINSQ_1:def 4;
then dom ssD = (dom s) +^ 1 by ORDINAL4:def 1;
hence A116: dom ssD = succ D by A14, ORDINAL2:31; :: thesis: ssD,y,r simplest_up_to dom ssD
let B be Ordinal; :: according to SURREALC:def 19 :: thesis: ( B in dom ssD implies ssD,y,r simplest_on_position B )
assume A117: B in dom ssD ; :: thesis: ssD,y,r simplest_on_position B
A118: dom s = (dom ssD) /\ (dom s) by ORDINAL7:1, A14, A116;
for o being object st o in dom s holds
s . o = ssD . o by ORDINAL4:def 1;
then A119: ssD | D = s by A118, FUNCT_1:46, A14;
A120: s | D = s by A14;

per cases ( B = D or B in D ) by A116, A117, ORDINAL1:8;

suppose A121: B = D ; :: thesis: ssD,y,r simplest_on_position B

ssD,y,r simplest_on_position D

proof

let sa be Surreal; :: according to SURREALC:def 18 :: thesis: ( sa = ssD . D implies ( ( 0 = D implies sa = 0_No ) & ( 0 <> D implies ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) ) ) ) )
assume A122: sa = ssD . D ; :: thesis: ( ( 0 = D implies sa = 0_No ) & ( 0 <> D implies ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) ) ) )
0 in dom <%sD%> by A115, TARSKI:def 1, CARD_1:49;
then ( ssD . (D +^ 0) = <%sD%> . 0 & <%sD%> . 0 = sD ) by A14, ORDINAL4:def 1;
then A123: sa = sD by A122, ORDINAL2:27;
thus ( 0 = D implies sa = 0_No ) by A9; :: thesis: ( 0 <> D implies ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) ) )
assume 0 <> D ; :: thesis: ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) )
thus sa in_meets_terms ssD,y,r,D by A113, A119, A120, Th76, A123; :: thesis: for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x
let x be uSurreal; :: thesis: ( x in_meets_terms ssD,y,r,D & x <> sa implies born sa in born x )
thus ( x in_meets_terms ssD,y,r,D & x <> sa implies born sa in born x ) by A119, A120, Th76, A114, A123; :: thesis: verum

end;

hence ssD,y,r simplest_on_position B by A121; :: thesis: verum

end;

suppose A124: B in D ; :: thesis: ssD,y,r simplest_on_position B

then A125: s | (succ B),y,r simplest_on_position B by A17, Th81;
ssD | (succ B) = s | (succ B) by A124, ORDINAL1:21, A119, RELAT_1:74;
hence ssD,y,r simplest_on_position B by A125, Th81; :: thesis: verum

end;

end;

end;

suppose not D is limit_ordinal ; :: thesis: ex s being uSurreal-Sequence st
( dom s = succ D & s,y,r simplest_up_to dom s )

then consider d being Ordinal such that
A126: D = succ d by ORDINAL1:29;
A127: d in D by A126, ORDINAL1:6;
consider s being uSurreal-Sequence such that
A128: dom s = succ d and
A129: s,y,r simplest_up_to dom s by ORDINAL1:def 2, A127, A2, A3;
A130: ( d in dom r & d in dom y ) by A127, XBOOLE_0:def 4, A3;
then ( r . d in rng r & y . d in rng y ) by FUNCT_1:def 3;
then reconsider yd = y . d as Surreal by SURREAL0:def 16;
A131: yd is positive by A130, Def15;
s . d in rng s by A128, A126, A127, FUNCT_1:def 3;
then reconsider sd = s . d as uSurreal by SURREALO:def 12;
set c = sd + ((uReal . (r . d)) * yd);
s,y,r simplest_on_position d by A129, ORDINAL1:6, A128;
then A132: ( ( 0 = d implies sd = 0_No ) & ( 0 <> d implies ( sd in_meets_terms s,y,r,d & ( for x being uSurreal st x in_meets_terms s,y,r,d & x <> sd holds
born sd in born x ) ) ) ) ;
defpred S₂[ Surreal] means $1 in_meets_terms s,y,r,D;
sd + ((uReal . (r . d)) * yd) in_meets_terms s,y,r,D

proof

let b be Ordinal; :: according to SURREALC:def 17 :: thesis: for sb, yb being Surreal st b in D & sb = s . b & yb = y . b holds
sd + ((uReal . (r . d)) * yd) is sb,yb,r . b _Term
let sb, yb be Surreal; :: thesis: ( b in D & sb = s . b & yb = y . b implies sd + ((uReal . (r . d)) * yd) is sb,yb,r . b _Term )
assume A133: ( b in D & sb = s . b & yb = y . b ) ; :: thesis: sd + ((uReal . (r . d)) * yd) is sb,yb,r . b _Term
A134: b c= d by A133, A126, ORDINAL1:22;
A135: yb is positive by A133, A5, Def15;

per cases ( b = d or b <> d ) ;

suppose b = d ; :: thesis: sd + ((uReal . (r . d)) * yd) is sb,yb,r . b _Term

hence sd + ((uReal . (r . d)) * yd) is sb,yb,r . b _Term by A135, Th83, A133; :: thesis: verum

end;

suppose b <> d ; :: thesis: sd + ((uReal . (r . d)) * yd) is sb,yb,r . b _Term

then A136: b in d by ORDINAL1:11, A134, XBOOLE_0:def 8;
A137: sd is sb,yb,r . b _Term by A136, A133, A132;
A138: yd infinitely< yb by A133, A5, A136, A127, Def16;
|.((uReal . (r . d)) * yd).| infinitely< yb

proof

per cases ( r . d = 0 or r . d <> 0 ) ;

suppose A139: r . d = 0 ; :: thesis: |.((uReal . (r . d)) * yd).| infinitely< yb

A140: 0_No <= yb by A135;
then A141: |.yb.| = yb by Def6;
A142: not |.yb.| == 0_No by A140, Def6, A135;
|.((uReal . (r . d)) * yd).| == 0_No by Def6, A139, SURREALN:47;
hence |.((uReal . (r . d)) * yd).| infinitely< yb by A141, A142, Th64; :: thesis: verum

end;

suppose r . d <> 0 ; :: thesis: |.((uReal . (r . d)) * yd).| infinitely< yb

hence |.((uReal . (r . d)) * yd).| infinitely< yb by A138, Th15, A131, Th66; :: thesis: verum

end;

end;

end;

then A143: |.(sd + (- (sb + ((uReal . (r . b)) * yb)))).| + |.((uReal . (r . d)) * yd).| infinitely< yb by A137, Th18;
(sd + ((uReal . (r . d)) * yd)) + (- (sb + ((uReal . (r . b)) * yb))) = (sd + (- (sb + ((uReal . (r . b)) * yb)))) + ((uReal . (r . d)) * yd) by SURREALR:37;
hence sd + ((uReal . (r . d)) * yd) is sb,yb,r . b _Term by Th11, A143, Th37; :: thesis: verum

end;

end;

end;

then A144: ex x being Surreal st S₂[x] ;
A145: for x, y, z being Surreal st x <= y & y <= z & S₂[x] & S₂[z] holds
S₂[y] by Th82, A3, XBOOLE_1:18;
consider sD being uSurreal such that
A146: S₂[sD] and
A147: for x being uSurreal st S₂[x] & x <> sD holds
born sD in born x from SURREALC:sch 1(A144, A145);
take ssD = s ^ <%sD%>; :: thesis: ( dom ssD = succ D & ssD,y,r simplest_up_to dom ssD )
A148: dom <%sD%> = 1 by AFINSQ_1:def 4;
then dom ssD = (dom s) +^ 1 by ORDINAL4:def 1;
hence A149: dom ssD = succ D by A128, A126, ORDINAL2:31; :: thesis: ssD,y,r simplest_up_to dom ssD
let B be Ordinal; :: according to SURREALC:def 19 :: thesis: ( B in dom ssD implies ssD,y,r simplest_on_position B )
assume A150: B in dom ssD ; :: thesis: ssD,y,r simplest_on_position B
A151: dom s = (dom ssD) /\ (dom s) by ORDINAL7:1, A128, A126, A149;
for o being object st o in dom s holds
s . o = ssD . o by ORDINAL4:def 1;
then A152: ssD | D = s by A151, FUNCT_1:46, A128, A126;
A153: s | D = s by A128, A126;

per cases ( B = D or B in D ) by A149, A150, ORDINAL1:8;

suppose A154: B = D ; :: thesis: ssD,y,r simplest_on_position B

ssD,y,r simplest_on_position D

proof

let sa be Surreal; :: according to SURREALC:def 18 :: thesis: ( sa = ssD . D implies ( ( 0 = D implies sa = 0_No ) & ( 0 <> D implies ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) ) ) ) )
assume A155: sa = ssD . D ; :: thesis: ( ( 0 = D implies sa = 0_No ) & ( 0 <> D implies ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) ) ) )
0 in dom <%sD%> by A148, TARSKI:def 1, CARD_1:49;
then ( ssD . (D +^ 0) = <%sD%> . 0 & <%sD%> . 0 = sD ) by A128, A126, ORDINAL4:def 1;
then A156: sa = sD by A155, ORDINAL2:27;
thus ( 0 = D implies sa = 0_No ) by A126; :: thesis: ( 0 <> D implies ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) ) )
assume 0 <> D ; :: thesis: ( sa in_meets_terms ssD,y,r,D & ( for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x ) )
thus sa in_meets_terms ssD,y,r,D by A156, A146, A152, A153, Th76; :: thesis: for x being uSurreal st x in_meets_terms ssD,y,r,D & x <> sa holds
born sa in born x
let x be uSurreal; :: thesis: ( x in_meets_terms ssD,y,r,D & x <> sa implies born sa in born x )
assume A157: ( x in_meets_terms ssD,y,r,D & x <> sa ) ; :: thesis: born sa in born x
thus born sa in born x by A147, A156, A157, A152, A153, Th76; :: thesis: verum

end;

hence ssD,y,r simplest_on_position B by A154; :: thesis: verum

end;

suppose A158: B in D ; :: thesis: ssD,y,r simplest_on_position B

then A159: s | (succ B),y,r simplest_on_position B by A128, A129, A126, Th81;
ssD | (succ B) = s | (succ B) by A158, ORDINAL1:21, A152, RELAT_1:74;
hence ssD,y,r simplest_on_position B by A159, Th81; :: thesis: verum

end;

end;

end;

end;

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence ex s being uSurreal-Sequence st
( dom s = succ ((dom r) /\ (dom y)) & s,y,r simplest_up_to dom s ) ; :: thesis: verum