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

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