let dA1, dA2 be ManySortedSet of Day A; :: thesis: ( ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & dA1 = 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)))] ) ) ) ) & ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & dA2 = 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)))] ) ) ) ) implies dA1 = dA2 )
deffunc H₁( Ordinal) -> Element of K10((Games $1)) = Day $1;
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)))];
given S1 being c=-monotone Function-yielding Sequence such that A21: ( dom S1 = succ A & dA1 = S1 . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S1 . B = SB & ( for x being object st x in Day B holds
SB . x = H₂(x,S1 | B) ) ) ) ) ; :: thesis: ( for S being c=-monotone Function-yielding Sequence holds
( not dom S = succ A or not dA2 = 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 x being object st
( x in Day B & not 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)))] ) ) ) ) ) or dA1 = dA2 )
given S2 being c=-monotone Function-yielding Sequence such that A22: ( dom S2 = succ A & dA2 = S2 . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S2 . B = SB & ( for x being object st x in Day B holds
SB . x = H₂(x,S2 | B) ) ) ) ) ; :: thesis: dA1 = dA2
A23: ( succ A c= dom S1 & succ A c= dom S2 ) by A21, A22;
A24: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S1 | B) ) ) by A21;
A25: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S2 | B) ) ) by A22;
S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A23, A24, A25);
then S1 | (succ A) = S2 by A22;
hence dA1 = dA2 by A21, A22; :: thesis: verum