deffunc H1( Ordinal) -> Element of bool (Games $1) = Day $1;
deffunc H2( object , Function-yielding c=-monotone Sequence) -> object = [((union (rng $2)) .: (R_ $1)),((union (rng $2)) .: (L_ $1))];
A1: for S being Function-yielding c=-monotone Sequence st ( for A being Ordinal st A in dom S holds
dom (S . A) = H1(A) ) holds
for A being Ordinal
for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(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) = H1(A) ) implies for A being Ordinal
for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(x,S) )
assume A2: for A being Ordinal st A in dom S holds
dom (S . A) = H1(A) ; :: thesis: for A being Ordinal
for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(x,S)
let A be Ordinal; :: thesis: for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(x,S)
let x be object ; :: thesis: ( x in dom (S . A) implies H2(x,S | A) = H2(x,S) )
assume A3: x in dom (S . A) ; :: thesis: H2(x,S | A) = H2(x,S)
S . A <> {} by A3;
then A4: A in dom S by FUNCT_1:def 2;
then A5: dom (S . A) = H1(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: now :: thesis: for y being object st y in L_ x holds
ex B being Ordinal st
( y in dom (S . B) & B in A )
let y be object ; :: thesis: ( y in L_ x implies ex B being Ordinal st
( y in dom (S . B) & B in A ) )
assume y in L_ x ; :: thesis: ex B being Ordinal st
( y in dom (S . B) & B in A )
then y in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
hence ex B being Ordinal st
( y in dom (S . B) & B in A ) by A7; :: thesis: verum
end;
now :: thesis: for y being object st y in R_ x holds
ex B being Ordinal st
( y in dom (S . B) & B in A )
let y be object ; :: thesis: ( y in R_ x implies ex B being Ordinal st
( y in dom (S . B) & B in A ) )
assume y in R_ x ; :: thesis: ex B being Ordinal st
( y in dom (S . B) & B in A )
then y in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
hence ex B being Ordinal st
( y in dom (S . B) & B in A ) by A7; :: thesis: verum
end;
then (union (rng (S | A))) .: (R_ x) = (union (rng S)) .: (R_ x) by Th3;
hence H2(x,S | A) = H2(x,S) by A9, Th3; :: thesis: verum
end;
A10: for A, B being Ordinal st A c= B holds
H1(A) c= H1(B) by SURREAL0:35;
consider S being Function-yielding c=-monotone Sequence such that
A11: ( dom S = succ A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H1(B) st
( S . B = SB & ( for x being object st x in H1(B) holds
SB . x = H2(x,S | B) ) ) ) ) from SURREALR:sch 1(A1, A10);
 A in succ A by ORDINAL1:8;
then consider SB being ManySortedSet of H1(A) such that
A12: ( S . A = SB & ( for x being object st x in H1(A) holds
SB . x = H2(x,S | A) ) ) by A11;
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 o being object st o in Day B holds
SB . o = [((union (rng (S | B))) .: (R_ o)),((union (rng (S | B))) .: (L_ o))] ) ) ) )
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 o being object st o in Day B holds
SB . o = [((union (rng (S | B))) .: (R_ o)),((union (rng (S | B))) .: (L_ o))] ) ) ) )
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 o being object st o in Day B holds
SB . o = [((union (rng (S | B))) .: (R_ o)),((union (rng (S | B))) .: (L_ o))] ) ) ) ) by A11, A12; :: thesis: verum