scheme :: ORDINAL2:sch 5
TSExist1{ F₁() -> Ordinal, F₂() -> object , F₃( Ordinal, set ) -> object , F₄( Ordinal, Sequence) -> object } :

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