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)))];
let S1 be c=-monotone Function-yielding Sequence; :: thesis: ( ( for B being Ordinal st B in dom S1 holds
ex SB being ManySortedSet of Day B st
( S1 . B = SB & ( for o being object st o in Day B holds
SB . o = [(Union (sqrtL ([((union (rng (S1 | B))) .: (L_ (NonNegativePart o))),((union (rng (S1 | B))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S1 | B))) .: (L_ (NonNegativePart o))),((union (rng (S1 | B))) .: (R_ (NonNegativePart o)))],o)))] ) ) ) implies for A being Ordinal st A in dom S1 holds
No_sqrt_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_sqrt_op A = S1 . A
let A be Ordinal; :: thesis: ( A in dom S1 implies No_sqrt_op A = S1 . A )
assume A2: A in dom S1 ; :: thesis: No_sqrt_op A = S1 . A
A3: succ A c= dom S1 by A2, ORDINAL1:21;
consider S2 being c=-monotone Function-yielding Sequence such that
A4: ( dom S2 = succ A & S2 . A = No_sqrt_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 Def6;
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_sqrt_op A = S1 . A by A4, A8, FUNCT_1:49; :: thesis: verum