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

for A being Ordinal holds F₄((succ A)) = F₂(A,F₄(A))

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)) ) ) )