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

for A being Ordinal holds F₄((succ A)) = F₂(A,F₄(A))

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)) ) ) )