deffunc H₁( Ordinal) -> Subset of (Day $1) = Positives $1;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (divL (||.$1.||,(union (rng $2))))),(Union (divR (||.$1.||,(union (rng $2)))))];
let S1 be c=-monotone Function-yielding Sequence; :: thesis: ( ( for B being Ordinal st B in dom S1 holds
ex SB being ManySortedSet of Positives B st
( S1 . B = SB & ( for o being object st o in Positives B holds
SB . o = [(Union (divL (||.o.||,(union (rng (S1 | B)))))),(Union (divR (||.o.||,(union (rng (S1 | B))))))] ) ) ) implies for A being Ordinal st A in dom S1 holds
No_inverse_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_inverse_op A = S1 . A
let A be Ordinal; :: thesis: ( A in dom S1 implies No_inverse_op A = S1 . A )
assume A2: A in dom S1 ; :: thesis: No_inverse_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_inverse_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 Def11;
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_inverse_op A = S1 . A by A4, A8, FUNCT_1:49; :: thesis: verum