scheme :: ORDINAL6:sch 1
CriticalNumber2{ F₁() -> Universe, F₂() -> Ordinal of F₁(), F₃() -> Ordinal-Sequence of omega,F₁(), F₄( Ordinal) -> Ordinal } :

( F₂() c= Union F₃() & F₄((Union F₃())) = Union F₃() & ( for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) )

provided

A1: omega in F₁() and
A2: for a being Ordinal st a in F₁() holds
F₄(a) in F₁() and
A3: for a, b being Ordinal st a in b & b in F₁() holds
F₄(a) in F₄(b) and
A4: for a being Ordinal of F₁() st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = F₄(b) ) holds
F₄(a) is_limes_of phi and
A5: F₃() . 0 = F₂() and
A6: for a being Ordinal st a in omega holds
F₃() . (succ a) = F₄((F₃() . a))