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

ex fi being Ordinal-Sequence st
( dom fi = F₁() & ( 0 in F₁() implies fi . 0 = F₂() ) & ( for A being Ordinal st succ A in F₁() holds
fi . (succ A) = F₃(A,(fi . A)) ) & ( for A being Ordinal st A in F₁() & A <> 0 & A is limit_ordinal holds
fi . A = F₄(A,(fi | A)) ) )