deffunc H₁( Ordinal) -> Subset of [:(Day $1),(Day $1):] = Triangle $1;
deffunc H₂( object , Function-yielding c=-monotone Sequence) -> object = [((union (rng $2)) .: ([:(L_ (L_ $1)),{(R_ $1)}:] \/ [:{(L_ $1)},(L_ (R_ $1)):])),((union (rng $2)) .: ([:(R_ (L_ $1)),{(R_ $1)}:] \/ [:{(L_ $1)},(R_ (R_ $1)):]))];
let S be Function-yielding c=-monotone Sequence; :: thesis: ( ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] ) ) ) implies for A being Ordinal st A in dom S holds
No_sum_op A = S . A )
assume A1: for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of H₁(B) st
( S . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S | B) ) ) ; :: thesis: for A being Ordinal st A in dom S holds
No_sum_op A = S . A
let A be Ordinal; :: thesis: ( A in dom S implies No_sum_op A = S . A )
assume A2: A in dom S ; :: thesis: No_sum_op A = S . A
consider S1 being Function-yielding c=-monotone Sequence such that
A3: ( dom S1 = succ A & No_sum_op A = S1 . A ) and
A4: 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 Def6;
A5: succ A c= dom S by A2, ORDINAL1:21;
A6: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S | B) ) ) by A1, A5;
A7: ( succ A c= dom S & succ A c= dom S1 ) by A2, ORDINAL1:21, A3;
A8: S | (succ A) = S1 | (succ A) from SURREALR:sch 2(A7, A6, A4);
A in succ A by ORDINAL1:8;
hence No_sum_op A = S . A by A3, A8, FUNCT_1:49; :: thesis: verum