scheme :: ORDINAL2:sch 10
TSResultL{ F₁() -> Sequence, F₂() -> Ordinal, F₃( Ordinal) -> set , F₄() -> set , F₅( Ordinal, set ) -> set , F₆( Ordinal, Sequence) -> set } :

F₃(F₂()) = F₆(F₂(),F₁())

provided

A1: for A being Ordinal
for x being object holds
( x = F₃(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F₄() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₅(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F₆(C,(L | C)) ) ) ) and
A2: ( F₂() <> 0 & F₂() is limit_ordinal ) and
A3: dom F₁() = F₂() and
A4: for A being Ordinal st A in F₂() holds
F₁() . A = F₃(A)