scheme :: ORDINAL2:sch 14
OSResult0{ F₁( Ordinal) -> Ordinal, F₂() -> Ordinal, F₃( Ordinal, Ordinal) -> Ordinal, F₄( Ordinal, Sequence) -> Ordinal } :

F₁(0) = 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)) ) ) )