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 ) } ];
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 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 ) } ] ) ) ) ) & 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 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 ) } ] ) ) ) ) implies O1 = O2 )
given S1 being Function-yielding c=-monotone Sequence such that A23: ( 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 x being object st
( x in Day B & not 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 ) } ] ) ) ) ) ) or O1 = O2 )
given S2 being Function-yielding c=-monotone Sequence such that A24: ( 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
A25: 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 A23;
A26: 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 A24;
A27: ( succ A c= dom S1 & succ A c= dom S2 ) by A23, A24;
S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A27, A25, A26);
then S1 = S2 | (succ A) by A23;
hence O1 = O2 by A23, A24; :: thesis: verum