deffunc H₁( Ordinal) -> Element of bool (Games $1) = Day $1;
deffunc H₂( object , Function-yielding c=-monotone Sequence) -> object = [({0_No} \/ { (((union (rng $2)) . xL) *' (uReal . r)) where xL is Element of L_ $1, r is Element of REAL : ( xL in L_ $1 & r is positive ) } ), { (((union (rng $2)) . xR) *' (uReal . r)) where xR is Element of R_ $1, r is Element of REAL : ( xR in R_ $1 & r is positive ) } ];
A1: 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 A2: 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 x be object ; :: thesis: ( x in dom (S . A) implies H₂(x,S | A) = H₂(x,S) )
assume A3: x in dom (S . A) ; :: thesis: H₂(x,S | A) = H₂(x,S)
S . A <> {} by A3;
then A4: A in dom S by FUNCT_1:def 2;
then A5: dom (S . A) = H₁(A) by A2;
then reconsider x = x as Surreal by A3;
A6: x = [(L_ x),(R_ x)] ;
A7: for y being object st y in (L_ x) \/ (R_ x) holds
ex B being Ordinal st
( y in dom (S . B) & B in A )

proof

let y be object ; :: thesis: ( y in (L_ x) \/ (R_ x) implies ex B being Ordinal st
( y in dom (S . B) & B in A ) )
assume y in (L_ x) \/ (R_ x) ; :: thesis: ex B being Ordinal st
( y in dom (S . B) & B in A )
then consider O being Ordinal such that
A8: ( O in A & y in Day O ) by A5, A3, A6, SURREAL0:46;
dom (S . O) = Day O by A2, A4, A8, ORDINAL1:10;
hence ex B being Ordinal st
( y in dom (S . B) & B in A ) by A8; :: thesis: verum

end;

A9: { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } c= { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } or y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } )
assume A10: y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ; :: thesis: y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) }
consider xL being Element of L_ x, r being Element of REAL such that
A11: ( y = ((union (rng S)) . xL) *' (uReal . r) & xL in L_ x & r is positive ) by A10;
xL in (L_ x) \/ (R_ x) by A11, XBOOLE_0:def 3;
then ex B being Ordinal st
( xL in dom (S . B) & B in A ) by A7;
then (union (rng (S | A))) . xL = (union (rng S)) . xL by SURREALR:5;
hence y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } by A11; :: thesis: verum

end;

{ (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } c= { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } or y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } )
assume A12: y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ; :: thesis: y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) }
consider xL being Element of L_ x, r being Element of REAL such that
A13: ( y = ((union (rng (S | A))) . xL) *' (uReal . r) & xL in L_ x & r is positive ) by A12;
xL in (L_ x) \/ (R_ x) by A13, XBOOLE_0:def 3;
then ex B being Ordinal st
( xL in dom (S . B) & B in A ) by A7;
then (union (rng (S | A))) . xL = (union (rng S)) . xL by SURREALR:5;
hence y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } by A13; :: thesis: verum

end;

then A14: L_ H₂(x,S | A) = L_ H₂(x,S) by A9, XBOOLE_0:def 10;
A15: { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } c= { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } or y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } )
assume A16: y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } ; :: thesis: y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) }
consider xL being Element of R_ x, r being Element of REAL such that
A17: ( y = ((union (rng S)) . xL) *' (uReal . r) & xL in R_ x & r is positive ) by A16;
xL in (L_ x) \/ (R_ x) by A17, XBOOLE_0:def 3;
then ex B being Ordinal st
( xL in dom (S . B) & B in A ) by A7;
then (union (rng (S | A))) . xL = (union (rng S)) . xL by SURREALR:5;
hence y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } by A17; :: thesis: verum

end;

{ (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } c= { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } or y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } )
assume A18: y in { (((union (rng (S | A))) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } ; :: thesis: y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) }
consider xL being Element of R_ x, r being Element of REAL such that
A19: ( y = ((union (rng (S | A))) . xL) *' (uReal . r) & xL in R_ x & r is positive ) by A18;
xL in (L_ x) \/ (R_ x) by A19, XBOOLE_0:def 3;
then ex B being Ordinal st
( xL in dom (S . B) & B in A ) by A7;
then (union (rng (S | A))) . xL = (union (rng S)) . xL by SURREALR:5;
hence y in { (((union (rng S)) . xL) *' (uReal . r)) where xL is Element of R_ x, r is Element of REAL : ( xL in R_ x & r is positive ) } by A19; :: thesis: verum

end;

hence H₂(x,S | A) = H₂(x,S) by A14, A15, XBOOLE_0:def 10; :: thesis: verum

end;

A20: for A, B being Ordinal st A c= B holds
H₁(A) c= H₁(B) by SURREAL0:35;
consider S being Function-yielding c=-monotone Sequence such that
A21: ( dom S = succ A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S | B) ) ) ) ) from SURREALR:sch 1(A1, A20);
A in succ A by ORDINAL1:8;
then consider SB being ManySortedSet of H₁(A) such that
A22: ( S . A = SB & ( for x being object st x in H₁(A) holds
SB . x = H₂(x,S | A) ) ) by A21;
take SB ; :: thesis: ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & SB = 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 = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) )
take S ; :: thesis: ( dom S = succ A & SB = 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 = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) )
thus ( dom S = succ A & SB = 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 = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) ) by A21, A22; :: thesis: verum