deffunc H₁( Ordinal) -> Element of K10((Games $1)) = Day $1;
A1: for A, B being Ordinal st A c= B holds
H₁(A) c= H₁(B) by SURREAL0:35;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (sqrtL ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1))),(Union (sqrtR ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1)))];
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)

proof

let S be c=-monotone Function-yielding Sequence; :: thesis: ( ( for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ) implies for A being Ordinal
for o being object st o in dom (S . A) holds
H₂(o,S | A) = H₂(o,S) )
assume A3: for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ; :: thesis: for A being Ordinal
for o being object st o in dom (S . A) holds
H₂(o,S | A) = H₂(o,S)
let A be Ordinal; :: thesis: for o being object st o in dom (S . A) holds
H₂(o,S | A) = H₂(o,S)
let o be object ; :: thesis: ( o in dom (S . A) implies H₂(o,S | A) = H₂(o,S) )
assume A4: o in dom (S . A) ; :: thesis: H₂(o,S | A) = H₂(o,S)
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 = NonNegativePart x;
A7: born x c= A by SURREAL0:def 18, A6, A4;
born (NonNegativePart x) c= born x by Th3;
then A8: born (NonNegativePart x) c= A by A7, XBOOLE_1:1;
A9: for a being object st a in L_ (NonNegativePart x) holds
ex B being Ordinal st
( a in dom (S . B) & B in A )

proof

let a be object ; :: thesis: ( a in L_ (NonNegativePart x) implies ex B being Ordinal st
( a in dom (S . B) & B in A ) )
assume A10: a in L_ (NonNegativePart x) ; :: thesis: ex B being Ordinal st
( a in dom (S . B) & B in A )
reconsider a = a as Surreal by A10, SURREAL0:def 16;
set b = born a;
a in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by XBOOLE_0:def 3, A10;
then A11: born a in born (NonNegativePart x) by SURREALO:1;
A12: a in Day (born a) by SURREAL0:def 18;
dom (S . (born a)) = H₁( born a) by A3, A11, A8, A5, ORDINAL1:10;
hence ex B being Ordinal st
( a in dom (S . B) & B in A ) by A12, A11, A8; :: thesis: verum

end;

A13: for a being object st a in R_ (NonNegativePart x) holds
ex B being Ordinal st
( a in dom (S . B) & B in A )

proof

let a be object ; :: thesis: ( a in R_ (NonNegativePart x) implies ex B being Ordinal st
( a in dom (S . B) & B in A ) )
assume A14: a in R_ (NonNegativePart x) ; :: thesis: ex B being Ordinal st
( a in dom (S . B) & B in A )
reconsider a = a as Surreal by A14, SURREAL0:def 16;
set b = born a;
a in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by XBOOLE_0:def 3, A14;
then A15: born a in born (NonNegativePart x) by SURREALO:1;
A16: a in Day (born a) by SURREAL0:def 18;
dom (S . (born a)) = H₁( born a) by A3, A15, A8, A5, ORDINAL1:10;
hence ex B being Ordinal st
( a in dom (S . B) & B in A ) by A15, A8, A16; :: thesis: verum

end;

A17: (union (rng S)) .: (L_ (NonNegativePart x)) = (union (rng (S | A))) .: (L_ (NonNegativePart x)) by A9, SURREALR:3;
(union (rng S)) .: (R_ (NonNegativePart x)) = (union (rng (S | A))) .: (R_ (NonNegativePart x)) by A13, SURREALR:3;
hence H₂(o,S | A) = H₂(o,S) by A17; :: thesis: verum

end;

consider S being c=-monotone Function-yielding Sequence such that
A18: dom S = succ A and
A19: 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
A20: ( S . A = SA & ( for o being object st o in H₁(A) holds
SA . o = H₂(o,S | A) ) ) by A19, ORDINAL1:6;
take SA ; :: thesis: ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x)))] ) ) ) )
take S ; :: thesis: ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x)))] ) ) ) )
thus ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x)))] ) ) ) ) by A18, A20, A19; :: thesis: verum