scheme :: ZF_REFLE:sch 3
UOSExist{ F₁() -> Universe, F₂() -> Ordinal of F₁(), F₃( Ordinal, Ordinal) -> Ordinal of F₁(), F₄( Ordinal, Sequence) -> Ordinal of F₁() } :

ex phi being Ordinal-Sequence of F₁() st
( phi . (0-element_of F₁()) = F₂() & ( for a being Ordinal of F₁() holds phi . (succ a) = F₃(a,(phi . a)) ) & ( for a being Ordinal of F₁() st a <> 0-element_of F₁() & a is limit_ordinal holds
phi . a = F₄(a,(phi | a)) ) )