let r be non-zero Sequence of REAL ; :: thesis:
let y be strictly_decreasing Surreal-Sequence; :: thesis:
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]

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
assume A3: D c= (dom r) /\ (dom y) ; :: thesis:
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;

suppose A6: D = {} ; :: thesis:

take s = <%0_No%>; :: thesis:
thus A7: dom s = succ D by A6, AFINSQ_1:def 4; :: thesis:
let A be Ordinal; :: according to SURREALC:def 16 :: thesis:
assume A8: A in dom s ; :: thesis:
let sa be Surreal; :: according to SURREALC:def 15 :: thesis:
assume sa = s . A ; :: thesis:
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:

end;

suppose A9: ( D is limit_ordinal & D <> {} ) ; :: thesis:

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:
assume A11: e in D ; :: thesis:
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:
thus S₂[e,s] by A12; :: thesis:

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:
assume o in rng S ; :: thesis:
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:

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:
assume A15: a in rng s ; :: thesis:
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:

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:
assume A18: E in D ; :: thesis:
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:
assume A22: o in succ E ; :: thesis:
then reconsider o = o as Ordinal ;
A23: (s | (succ E)) . o = s . o by A22, FUNCT_1:49;

per cases by A22, ORDINAL1:8;

suppose A24: o in E ; :: thesis:

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, Th77; :: thesis:

end;

suppose o = E ; :: thesis:

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

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, Th80; :: thesis:

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))) * (No_omega^ ya))) + (No_omega^ 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:
assume A33: e in D ; :: thesis:
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))) * (No_omega^ ya))) + (No_omega^ ya); :: thesis:
thus S₄[e,o] ; :: thesis:

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:
assume A37: o in rng upp ; :: thesis:
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:

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

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))) * (No_omega^ ya))) + (- (No_omega^ ya)) ) );
A54: for e being object st e in D holds
ex o being object st S₅[e,o]

proof

let e be object ; :: thesis:
assume A55: e in D ; :: thesis:
reconsider E = e as Ordinal by A55;
succ E in D by A55, 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))) * (No_omega^ ya))) + (- (No_omega^ ya)); :: thesis:
thus S₅[e,o] ; :: thesis:

end;

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

proof

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

end;

A60: 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

end;

A78: 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:
assume A79: A in D ; :: thesis:
let lA, uA be Surreal; :: thesis:
assume A80: ( lA = low . A & uA = upp . A ) ; :: thesis:
succ A in D by A79, 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;
set NA = No_omega^ yA;
A81: ( lA = (sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (- (No_omega^ yA)) & uA = (sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (No_omega^ yA) ) by A79, A80, A57, A35;
( - (No_omega^ yA) <= - 0_No & - 0_No = 0_No ) by SURREALI:def 8, SURREALR:10;
then - (No_omega^ yA) < No_omega^ yA by SURREALI:def 8, SURREALO:4;
hence lA < uA by A81, SURREALR:44; :: thesis:

end;

A82: rng low << rng upp

proof

let l, u be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A83: ( l in rng low & u in rng upp ) ; :: thesis:
consider A being object such that
A84: ( A in dom low & low . A = l ) by A83, FUNCT_1:def 3;
consider B being object such that
A85: ( B in dom upp & upp . B = u ) by A83, FUNCT_1:def 3;
reconsider A = A, B = B as Ordinal by A84, A85, A56, A34;
reconsider lowB = low . B, uppA = upp . A as Surreal by A84, A85, A56, A57, A34, A35;

per cases by ORDINAL1:14;

suppose A = B ; :: thesis:

hence not u <= l by A84, A85, A78, A56; :: thesis:

end;

suppose A in B ; :: thesis:

then ( l < lowB & lowB <= u ) by A60, A84, A85, A34, A78;
hence not u <= l by SURREALO:4; :: thesis:

end;

suppose B in A ; :: thesis:

then ( l <= uppA & uppA < u ) by A38, A84, A85, A56, A78;
hence not u <= l by SURREALO:4; :: thesis:

end;

consider M being Ordinal such that
A86: 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, A58, SURREAL0:47;
[(rng low),(rng upp)] in Day M by A82, A86, 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 14 :: thesis:
let sb, yb be Surreal; :: thesis:
assume A87: ( A in D & sb = s . A & yb = y . A ) ; :: thesis:
reconsider lowA = low . A, uppA = upp . A as Surreal by A87, A57, A35;
A88: succ A in D by A87, 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;
set NA = No_omega^ yA;
A89: ( lowA = (sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (- (No_omega^ yA)) & uppA = (sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (No_omega^ yA) ) by A87, A57, A35;
A90: r . A in rng r by A87, A4, FUNCT_1:def 3;
s,y,r simplest_on_position succ A by A31, A87, A9, ORDINAL1:28;
then A91: sA in_meets_terms s,y,r, succ A ;
sA is sb,yb,r . A _term by ORDINAL1:6, A87, A91;
then A92: |.(sA - (sb + ((uReal . (r . A)) * (No_omega^ yb)))).| infinitely< No_omega^ yb by Th73;
yA < yb by ORDINAL1:6, A88, A87, Def11, A5;
then A93: No_omega^ yA infinitely< No_omega^ yb by Lm5;
A94: ( lowA in rng low & uppA in rng upp ) by A87, A56, A34, FUNCT_1:def 3;
A95: ( L_ rLU << {rLU} & {rLU} << R_ rLU & rLU in {rLU} ) by SURREALO:11, TARSKI:def 1;
then - rLU < - ((sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (- (No_omega^ yA))) by A94, A89, SURREALR:10;
then A96: (- rLU) + (sb + ((uReal . (r . A)) * (No_omega^ yb))) <= (- ((sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (- (No_omega^ yA)))) + (sb + ((uReal . (r . A)) * (No_omega^ yb))) by SURREALR:44;
A97: (- rLU) + (sb + ((uReal . (r . A)) * (No_omega^ yb))) = (- rLU) + (- (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))))
.= - (rLU + (- (sb + ((uReal . (r . A)) * (No_omega^ yb))))) by SURREALR:40 ;
A98: (- ((sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (- (No_omega^ yA)))) + (sb + ((uReal . (r . A)) * (No_omega^ yb))) = ((- (sA + ((uReal . (r . (succ A))) * (No_omega^ yA)))) + (- (- (No_omega^ yA)))) + (sb + ((uReal . (r . A)) * (No_omega^ yb))) by SURREALR:40
.= (((- sA) + (- ((uReal . (r . (succ A))) * (No_omega^ yA)))) + (No_omega^ yA)) + (sb + ((uReal . (r . A)) * (No_omega^ yb))) by SURREALR:40
.= ((- sA) + ((- ((uReal . (r . (succ A))) * (No_omega^ yA))) + (No_omega^ yA))) + (sb + ((uReal . (r . A)) * (No_omega^ yb))) by SURREALR:37
.= ((- sA) + (- (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))))) + ((- ((uReal . (r . (succ A))) * (No_omega^ yA))) + (No_omega^ yA)) by SURREALR:37
.= (- (sA + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))))) + ((- ((uReal . (r . (succ A))) * (No_omega^ yA))) + (No_omega^ yA)) by SURREALR:40 ;
A99: 0_No <= No_omega^ yA by SURREALI:def 8;
then A100: No_omega^ yA = |.(No_omega^ yA).| by Def6;
A101: |.((uReal . (r . (succ A))) * (No_omega^ yA)).| infinitely< No_omega^ yb by A93, A99, Th53;
then |.((No_omega^ yA) + ((uReal . (r . (succ A))) * (No_omega^ yA))).| infinitely< No_omega^ yb by A93, Th41, A100;
then A102: |.((sA + (- (sb + ((uReal . (r . A)) * (No_omega^ yb))))) + ((No_omega^ yA) + ((uReal . (r . (succ A))) * (No_omega^ yA)))).| infinitely< No_omega^ yb by A92, Th41;
A103: |.(- (sA + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))))).| infinitely< No_omega^ yb by A92, Th42;
|.((No_omega^ yA) - ((uReal . (r . (succ A))) * (No_omega^ yA))).| infinitely< No_omega^ yb by A93, Th43, A100, A101;
then A104: |.((- (sA + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))))) + ((No_omega^ yA) + (- ((uReal . (r . (succ A))) * (No_omega^ yA))))).| infinitely< No_omega^ yb by A103, Th41;
(- (sA + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))))) + ((No_omega^ yA) + (- ((uReal . (r . (succ A))) * (No_omega^ yA)))) infinitely< No_omega^ yb by Th34, Th11, A104;
then A105: - (rLU + (- (sb + ((uReal . (r . A)) * (No_omega^ yb))))) infinitely< No_omega^ yb by A97, A96, A98, Th11;
A106: rLU + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))) <= ((sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (No_omega^ yA)) + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))) by A94, A95, A89, SURREALR:44;
A107: ((sA + ((uReal . (r . (succ A))) * (No_omega^ yA))) + (No_omega^ yA)) + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))) = (sA + (((uReal . (r . (succ A))) * (No_omega^ yA)) + (No_omega^ yA))) + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))) by SURREALR:37
.= (sA + (- (sb + ((uReal . (r . A)) * (No_omega^ yb))))) + ((No_omega^ yA) + ((uReal . (r . (succ A))) * (No_omega^ yA))) by SURREALR:37 ;
(sA + (- (sb + ((uReal . (r . A)) * (No_omega^ yb))))) + ((No_omega^ yA) + ((uReal . (r . (succ A))) * (No_omega^ yA))) infinitely< No_omega^ yb by Th34, A102, Th11;
then rLU + (- (sb + ((uReal . (r . A)) * (No_omega^ yb)))) infinitely< No_omega^ yb by A107, A106, Th11;
then |.(rLU - (sb + ((uReal . (r . A)) * (No_omega^ yb)))).| infinitely< No_omega^ yb by Def6, A105;
hence rLU is sb,yb,r . A _term by A90, Th73; :: thesis:

end;

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

per cases by A113, A114, ORDINAL1:8;

suppose A118: B = D ; :: thesis:

ssD,y,r simplest_on_position D

proof

let sa be Surreal; :: according to SURREALC:def 15 :: thesis:
assume A119: sa = ssD . D ; :: thesis:
0 in dom <%sD%> by A112, TARSKI:def 1, CARD_1:49;
then ( ssD . (D +^ 0) = <%sD%> . 0 & <%sD%> . 0 = sD ) by A14, ORDINAL4:def 1;
then A120: sa = sD by A119, ORDINAL2:27;
thus ( 0 = D implies sa = 0_No ) by A9; :: thesis:
assume 0 <> D ; :: thesis:
thus sa in_meets_terms ssD,y,r,D by A110, A116, A117, Th75, A120; :: thesis:
let x be uSurreal; :: thesis:
thus ( x in_meets_terms ssD,y,r,D & x <> sa implies born sa in born x ) by A116, A117, Th75, A111, A120; :: thesis:

end;

hence ssD,y,r simplest_on_position B by A118; :: thesis:

end;

suppose A121: B in D ; :: thesis:

then A122: s | (succ B),y,r simplest_on_position B by A17, Th80;
ssD | (succ B) = s | (succ B) by A121, ORDINAL1:21, A116, RELAT_1:74;
hence ssD,y,r simplest_on_position B by A122, Th80; :: thesis:

end;

suppose not D is limit_ordinal ; :: thesis:

then consider d being Ordinal such that
A123: D = succ d by ORDINAL1:29;
A124: d in D by A123, ORDINAL1:6;
consider s being uSurreal-Sequence such that
A125: dom s = succ d and
A126: s,y,r simplest_up_to dom s by ORDINAL1:def 2, A124, A2, A3;
( d in dom r & d in dom y ) by A124, XBOOLE_0:def 4, A3;
then A127: ( 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;
s . d in rng s by A125, A123, A124, FUNCT_1:def 3;
then reconsider sd = s . d as uSurreal by SURREALO:def 12;
set c = sd + ((uReal . (r . d)) * (No_omega^ yd));
s,y,r simplest_on_position d by A126, ORDINAL1:6, A125;
then A128: ( ( 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)) * (No_omega^ yd)) in_meets_terms s,y,r,D

proof

let b be Ordinal; :: according to SURREALC:def 14 :: thesis:
let sb, yb be Surreal; :: thesis:
assume A129: ( b in D & sb = s . b & yb = y . b ) ; :: thesis:
A130: b c= d by A129, A123, ORDINAL1:22;

per cases ;

suppose b = d ; :: thesis:

hence sd + ((uReal . (r . d)) * (No_omega^ yd)) is sb,yb,r . b _term by A127, Th69, A129; :: thesis:

end;

suppose b <> d ; :: thesis:

then A131: b in d by ORDINAL1:11, A130, XBOOLE_0:def 8;
A132: sd is sb,yb,r . b _term by A131, A129, A128;
A133: r . b in rng r by A129, A4, FUNCT_1:def 3;
A134: |.(sd - (sb + ((uReal . (r . b)) * (No_omega^ yb)))).| infinitely< No_omega^ yb by A132, Th73;
A135: No_omega^ yd infinitely< No_omega^ yb by Th25, A129, Def11, A5, A131, A124;
|.((uReal . (r . d)) * (No_omega^ yd)).| infinitely< No_omega^ yb by A127, Th66, A135, Th15;
then A136: |.(sd + (- (sb + ((uReal . (r . b)) * (No_omega^ yb))))).| + |.((uReal . (r . d)) * (No_omega^ yd)).| infinitely< No_omega^ yb by A134, Th18;
(sd + ((uReal . (r . d)) * (No_omega^ yd))) + (- (sb + ((uReal . (r . b)) * (No_omega^ yb)))) = (sd + (- (sb + ((uReal . (r . b)) * (No_omega^ yb))))) + ((uReal . (r . d)) * (No_omega^ yd)) by SURREALR:37;
then |.((sd + ((uReal . (r . d)) * (No_omega^ yd))) - (sb + ((uReal . (r . b)) * (No_omega^ yb)))).| infinitely< No_omega^ yb by Th11, A136, Th37;
hence sd + ((uReal . (r . d)) * (No_omega^ yd)) is sb,yb,r . b _term by A133, Th73; :: thesis:

end;

then A137: ex x being Surreal st S₂[x] ;
A138: for x, y, z being Surreal st x <= y & y <= z & S₂[x] & S₂[z] holds
S₂[y] by Th81, A3, XBOOLE_1:18;
consider sD being uSurreal such that
A139: S₂[sD] and
A140: for x being uSurreal st S₂[x] & x <> sD holds
born sD in born x from SURREALC:sch 1(A137, A138);
take ssD = s ^ <%sD%>; :: thesis:
A141: dom <%sD%> = 1 by AFINSQ_1:def 4;
then dom ssD = (dom s) +^ 1 by ORDINAL4:def 1;
hence A142: dom ssD = succ D by A125, A123, ORDINAL2:31; :: thesis:
let B be Ordinal; :: according to SURREALC:def 16 :: thesis:
assume A143: B in dom ssD ; :: thesis:
A144: dom s = (dom ssD) /\ (dom s) by ORDINAL7:1, A125, A123, A142;
for o being object st o in dom s holds
s . o = ssD . o by ORDINAL4:def 1;
then A145: ssD | D = s by A144, FUNCT_1:46, A125, A123;
A146: s | D = s by A125, A123;

per cases by A142, A143, ORDINAL1:8;

suppose A147: B = D ; :: thesis:

ssD,y,r simplest_on_position D

proof

let sa be Surreal; :: according to SURREALC:def 15 :: thesis:
assume A148: sa = ssD . D ; :: thesis:
0 in dom <%sD%> by A141, TARSKI:def 1, CARD_1:49;
then ( ssD . (D +^ 0) = <%sD%> . 0 & <%sD%> . 0 = sD ) by A125, A123, ORDINAL4:def 1;
then A149: sa = sD by A148, ORDINAL2:27;
thus ( 0 = D implies sa = 0_No ) by A123; :: thesis:
assume 0 <> D ; :: thesis:
thus sa in_meets_terms ssD,y,r,D by A149, A139, A145, A146, Th75; :: thesis:
let x be uSurreal; :: thesis:
assume A150: ( x in_meets_terms ssD,y,r,D & x <> sa ) ; :: thesis:
thus born sa in born x by A140, A149, A150, A145, A146, Th75; :: thesis:

end;

hence ssD,y,r simplest_on_position B by A147; :: thesis:

end;

suppose A151: B in D ; :: thesis:

then A152: s | (succ B),y,r simplest_on_position B by A125, A126, A123, Th80;
ssD | (succ B) = s | (succ B) by A151, ORDINAL1:21, A145, RELAT_1:74;
hence ssD,y,r simplest_on_position B by A152, Th80; :: thesis:

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: