scheme :: ZF_REFLE:sch 3
UOSExist{ F1() -> Universe, F2() -> Ordinal of F1(), F3( Ordinal, Ordinal) -> Ordinal of F1(), F4( Ordinal, Sequence) -> Ordinal of F1() } :
ex phi being Ordinal-Sequence of F1() st
( phi . (0-element_of F1()) = F2() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )