deffunc H₁( Ordinal) -> Element of bool (Games $1) = Day $1;
deffunc H₂( object , Function-yielding c=-monotone Sequence) -> object = [((union (rng $2)) .: (R_ $1)),((union (rng $2)) .: (L_ $1))];
let O1, O2 be ManySortedSet of H₁(A); :: thesis: ( ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & O1 = 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))] ) ) ) ) & ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & O2 = 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))] ) ) ) ) implies O1 = O2 )
given S1 being Function-yielding c=-monotone Sequence such that A13: ( dom S1 = succ A & S1 . A = O1 & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S1 | B) ) ) ) ) ; :: thesis: ( for S being Function-yielding c=-monotone Sequence holds
( not dom S = succ A or not O2 = S . A or ex B being Ordinal st
( B in succ A & ( for SB being ManySortedSet of Day B holds
( not S . B = SB or ex o being object st
( o in Day B & not SB . o = [((union (rng (S | B))) .: (R_ o)),((union (rng (S | B))) .: (L_ o))] ) ) ) ) ) or O1 = O2 )
given S2 being Function-yielding c=-monotone Sequence such that A14: ( dom S2 = succ A & S2 . A = O2 & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S2 | B) ) ) ) ) ; :: thesis: O1 = O2
A15: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S1 | B) ) ) by A13;
A16: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S2 | B) ) ) by A14;
A17: ( succ A c= dom S1 & succ A c= dom S2 ) by A13, A14;
S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A17, A15, A16);
then S1 = S2 | (succ A) by A13;
hence O1 = O2 by A13, A14; :: thesis: verum