scheme :: ORDINAL2:sch 11
OSExist{ F1() -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, Sequence) -> Ordinal } :
ex fi being Ordinal-Sequence st
( dom fi = F1() & ( 0 in F1() implies fi . 0 = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )