deffunc H₁( Ordinal) -> Subset of [:(Day $1),(Day $1):] = Triangle $1;
deffunc H₂( object , Function-yielding c=-monotone Sequence) -> object = [( { ((((union (rng $2)) . [xL,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yL])) +' (-' ((union (rng $2)) . [xL,yL]))) where xL is Element of L_ (L_ $1), yL is Element of L_ (R_ $1) : ( xL in L_ (L_ $1) & yL in L_ (R_ $1) ) } \/ { ((((union (rng $2)) . [xR,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yR])) +' (-' ((union (rng $2)) . [xR,yR]))) where xR is Element of R_ (L_ $1), yR is Element of R_ (R_ $1) : ( xR in R_ (L_ $1) & yR in R_ (R_ $1) ) } ),( { ((((union (rng $2)) . [xL,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yR])) +' (-' ((union (rng $2)) . [xL,yR]))) where xL is Element of L_ (L_ $1), yR is Element of R_ (R_ $1) : ( xL in L_ (L_ $1) & yR in R_ (R_ $1) ) } \/ { ((((union (rng $2)) . [xR,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yL])) +' (-' ((union (rng $2)) . [xR,yL]))) where xR is Element of R_ (L_ $1), yL is Element of L_ (R_ $1) : ( xR in R_ (L_ $1) & yL in L_ (R_ $1) ) } )];
let it1, it2 be ManySortedSet of Triangle A; :: thesis: ( ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & it1 = S . A & ( for B being Ordinal st B in succ A 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))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) ) & ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & it2 = S . A & ( for B being Ordinal st B in succ A 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))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) ) implies it1 = it2 )
given S1 being Function-yielding c=-monotone Sequence such that A35: ( dom S1 = succ A & it1 = S1 . A ) and
A36: 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) ) ) ; :: thesis: ( for S being Function-yielding c=-monotone Sequence holds
( not dom S = succ A or not it2 = S . A or ex B being Ordinal st
( B in succ A & ( for SB being ManySortedSet of Triangle B holds
( not S . B = SB or ex x being object st
( x in Triangle B & not SB . x = [( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) ) ) or it1 = it2 )
given S2 being Function-yielding c=-monotone Sequence such that A37: ( dom S2 = succ A & it2 = S2 . A ) and
A38: 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) ) ) ; :: thesis: it1 = it2
A39: ( succ A c= dom S1 & succ A c= dom S2 ) by A35, A37;
S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A39, A36, A38);
then S1 | (succ A) = S2 by A37;
hence it1 = it2 by A35, A37; :: thesis: verum