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

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

provided

A1: for A, B being Ordinal holds
( B = F₃(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . 0 = F₄() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F₅(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = F₆(C,(fi | 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)