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 S1 be Function-yielding c=-monotone Sequence; :: thesis: ( ( for B being Ordinal st B in dom S1 holds
ex SB being ManySortedSet of Day B st
( S1 . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S1 | 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 (S1 | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) implies for A being Ordinal st A in dom S1 holds
No_omega_op A = S1 . A )
assume A1: for B being Ordinal st B in dom S1 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 A being Ordinal st A in dom S1 holds
No_omega_op A = S1 . A
let A be Ordinal; :: thesis: ( A in dom S1 implies No_omega_op A = S1 . A )
assume A2: A in dom S1 ; :: thesis: No_omega_op A = S1 . A
A3: succ A c= dom S1 by A2, ORDINAL1:21;
consider S2 being Function-yielding c=-monotone Sequence such that
A4: ( dom S2 = succ A & S2 . A = No_omega_op A & ( 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 Def4;
A5: 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 A1, A3;
A6: 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 A4;
A7: ( succ A c= dom S1 & succ A c= dom S2 ) by A2, ORDINAL1:21, A4;
A8: S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A7, A5, A6);
A in succ A by ORDINAL1:8;
hence No_omega_op A = S1 . A by A4, A8, FUNCT_1:49; :: thesis: verum