deffunc H₁( Ordinal) -> Subset of [:(Day $1),(Day $1):] = Triangle $1;
deffunc H₂( object , Function-yielding c=-monotone Sequence) -> object = [((union (rng $2)) .: ([:(L_ (L_ $1)),{(R_ $1)}:] \/ [:{(L_ $1)},(L_ (R_ $1)):])),((union (rng $2)) .: ([:(R_ (L_ $1)),{(R_ $1)}:] \/ [:{(L_ $1)},(R_ (R_ $1)):]))];
A1: for A, B being Ordinal st A c= B holds
H₁(A) c= H₁(B) by Th25;
A2: for S being Function-yielding c=-monotone Sequence st ( for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ) holds
for A being Ordinal
for x being object st x in dom (S . A) holds
H₂(x,S | A) = H₂(x,S)

proof

let S be Function-yielding c=-monotone Sequence; :: thesis: ( ( for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ) implies for A being Ordinal
for x being object st x in dom (S . A) holds
H₂(x,S | A) = H₂(x,S) )
assume A3: for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ; :: thesis: for A being Ordinal
for x being object st x in dom (S . A) holds
H₂(x,S | A) = H₂(x,S)
let A be Ordinal; :: thesis: for x being object st x in dom (S . A) holds
H₂(x,S | A) = H₂(x,S)
let a be object ; :: thesis: ( a in dom (S . A) implies H₂(a,S | A) = H₂(a,S) )
assume A4: a in dom (S . A) ; :: thesis: H₂(a,S | A) = H₂(a,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 consider x, y being object such that
A7: ( x in Day A & y in Day A & a = [x,y] ) by A4, ZFMISC_1:def 2;
reconsider x = x, y = y as Surreal by A7;
A8: (born x) (+) (born y) c= A by A7, A6, A4, Def5;
set LL = [:(L_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(L_ (R_ a)):];
for b being object st b in [:(L_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(L_ (R_ a)):] holds
ex B being Ordinal st
( b in dom (S . B) & B in A )

proof

let b be object ; :: thesis: ( b in [:(L_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(L_ (R_ a)):] implies ex B being Ordinal st
( b in dom (S . B) & B in A ) )
assume A9: b in [:(L_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(L_ (R_ a)):] ; :: thesis: ex B being Ordinal st
( b in dom (S . B) & B in A )

per cases ( b in [:(L_ (L_ a)),{(R_ a)}:] or b in [:{(L_ a)},(L_ (R_ a)):] ) by A9, XBOOLE_0:def 3;

suppose b in [:(L_ (L_ a)),{(R_ a)}:] ; :: thesis: ex B being Ordinal st
( b in dom (S . B) & B in A )

then consider l, r being object such that
A10: ( l in L_ x & r in {y} & b = [l,r] ) by A7, ZFMISC_1:def 2;
reconsider l = l as Surreal by A10, SURREAL0:def 16;
set B = (born l) (+) (born y);
take (born l) (+) (born y) ; :: thesis: ( b in dom (S . ((born l) (+) (born y))) & (born l) (+) (born y) in A )
l in (L_ x) \/ (R_ x) by A10, XBOOLE_0:def 3;
then A11: (born l) (+) (born y) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then A12: dom (S . ((born l) (+) (born y))) = H₁((born l) (+) (born y)) by A8, A3, A5, ORDINAL1:10;
[l,y] in H₁((born l) (+) (born y)) by Def5;
hence ( b in dom (S . ((born l) (+) (born y))) & (born l) (+) (born y) in A ) by A12, A10, A11, A8, TARSKI:def 1; :: thesis: verum

end;

suppose b in [:{(L_ a)},(L_ (R_ a)):] ; :: thesis: ex B being Ordinal st
( b in dom (S . B) & B in A )

then consider l, r being object such that
A13: ( l in {x} & r in L_ y & b = [l,r] ) by A7, ZFMISC_1:def 2;
reconsider r = r as Surreal by A13, SURREAL0:def 16;
set B = (born x) (+) (born r);
take (born x) (+) (born r) ; :: thesis: ( b in dom (S . ((born x) (+) (born r))) & (born x) (+) (born r) in A )
r in (L_ y) \/ (R_ y) by A13, XBOOLE_0:def 3;
then A14: (born x) (+) (born r) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then A15: dom (S . ((born x) (+) (born r))) = H₁((born x) (+) (born r)) by A8, A3, A5, ORDINAL1:10;
[x,r] in H₁((born x) (+) (born r)) by Def5;
hence ( b in dom (S . ((born x) (+) (born r))) & (born x) (+) (born r) in A ) by A15, A13, A14, A8, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A16: (union (rng (S | A))) .: ([:(L_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(L_ (R_ a)):]) = (union (rng S)) .: ([:(L_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(L_ (R_ a)):]) by Th3;
set RR = [:(R_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(R_ (R_ a)):];
for b being object st b in [:(R_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(R_ (R_ a)):] holds
ex B being Ordinal st
( b in dom (S . B) & B in A )

proof

let b be object ; :: thesis: ( b in [:(R_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(R_ (R_ a)):] implies ex B being Ordinal st
( b in dom (S . B) & B in A ) )
assume A17: b in [:(R_ (L_ a)),{(R_ a)}:] \/ [:{(L_ a)},(R_ (R_ a)):] ; :: thesis: ex B being Ordinal st
( b in dom (S . B) & B in A )

per cases ( b in [:(R_ (L_ a)),{(R_ a)}:] or b in [:{(L_ a)},(R_ (R_ a)):] ) by A17, XBOOLE_0:def 3;

suppose b in [:(R_ (L_ a)),{(R_ a)}:] ; :: thesis: ex B being Ordinal st
( b in dom (S . B) & B in A )

then consider l, r being object such that
A18: ( l in R_ x & r in {y} & b = [l,r] ) by A7, ZFMISC_1:def 2;
reconsider l = l as Surreal by A18, SURREAL0:def 16;
set B = (born l) (+) (born y);
take (born l) (+) (born y) ; :: thesis: ( b in dom (S . ((born l) (+) (born y))) & (born l) (+) (born y) in A )
l in (L_ x) \/ (R_ x) by A18, XBOOLE_0:def 3;
then A19: (born l) (+) (born y) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then A20: dom (S . ((born l) (+) (born y))) = H₁((born l) (+) (born y)) by A8, A3, A5, ORDINAL1:10;
[l,y] in H₁((born l) (+) (born y)) by Def5;
hence ( b in dom (S . ((born l) (+) (born y))) & (born l) (+) (born y) in A ) by A20, A18, A19, A8, TARSKI:def 1; :: thesis: verum

end;

suppose b in [:{(L_ a)},(R_ (R_ a)):] ; :: thesis: ex B being Ordinal st
( b in dom (S . B) & B in A )

then consider l, r being object such that
A21: ( l in {x} & r in R_ y & b = [l,r] ) by A7, ZFMISC_1:def 2;
reconsider r = r as Surreal by A21, SURREAL0:def 16;
set B = (born x) (+) (born r);
take (born x) (+) (born r) ; :: thesis: ( b in dom (S . ((born x) (+) (born r))) & (born x) (+) (born r) in A )
r in (L_ y) \/ (R_ y) by A21, XBOOLE_0:def 3;
then A22: (born x) (+) (born r) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then A23: dom (S . ((born x) (+) (born r))) = H₁((born x) (+) (born r)) by A8, A3, A5, ORDINAL1:10;
[x,r] in H₁((born x) (+) (born r)) by Def5;
hence ( b in dom (S . ((born x) (+) (born r))) & (born x) (+) (born r) in A ) by A23, A21, A22, A8, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence H₂(a,S | A) = H₂(a,S) by A16, Th3; :: thesis: verum

end;

consider S being Function-yielding c=-monotone Sequence such that
A24: dom S = succ A and
A25: for A1 being Ordinal st A1 in succ A holds
ex SA1 being ManySortedSet of H₁(A1) st
( S . A1 = SA1 & ( for x being object st x in H₁(A1) holds
SA1 . x = H₂(x,S | A1) ) ) from SURREALR:sch 1(A2, A1);
consider SA being ManySortedSet of H₁(A) such that
A26: S . A = SA and
for x being object st x in H₁(A) holds
SA . x = H₂(x,S | A) by A25, ORDINAL1:6;
take SA ; :: thesis: ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ 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 Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] ) ) ) )
thus ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] ) ) ) ) by A24, A26, A25; :: thesis: verum