scheme :: ORDINAL5:sch 2
CriticalNumber3{ F1() -> Ordinal, F2( Ordinal) -> Ordinal } :
ex a being Ordinal st
( F1() in a & F2(a) = a )
provided
A1: for a, b being Ordinal st a in b holds
F2(a) in F2(b) and
A2: for a being Ordinal 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 = F2(b) ) holds
F2(a) is_limes_of phi