scheme :: ORDINAL2:sch 8
TSResult0{ F₁( Ordinal) -> set , F₂() -> set , F₃( Ordinal, set ) -> set , F₄( Ordinal, Sequence) -> set } :

F₁(0) = F₂()

provided

A1: for A being Ordinal
for x being object holds
( x = F₁(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F₂() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) )