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

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