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 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 o being object st o in Day B holds
SB . o = [((union (rng (S1 | B))) .: (R_ o)),((union (rng (S1 | B))) .: (L_ o))] ) ) ) implies for A being Ordinal st A in dom S1 holds
No_opposite_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_opposite_op A = S1 . A
let A be Ordinal; :: thesis: ( A in dom S1 implies No_opposite_op A = S1 . A )
assume A2: A in dom S1 ; :: thesis: No_opposite_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_opposite_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 Def2;
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_opposite_op A = S1 . A by A4, A8, FUNCT_1:49; :: thesis: verum