scheme :: ORDINAL2:sch 4
TSUniq1{ F₁() -> Ordinal, F₂() -> object , F₃( Ordinal, set ) -> object , F₄( Ordinal, Sequence) -> object , F₅() -> Sequence, F₆() -> Sequence } :

F₅() = F₆()

provided

A1: dom F₅() = F₁() and
A2: ( 0 in F₁() implies F₅() . 0 = F₂() ) and
A3: for A being Ordinal st succ A in F₁() holds
F₅() . (succ A) = F₃(A,(F₅() . A)) and
A4: for A being Ordinal st A in F₁() & A <> 0 & A is limit_ordinal holds
F₅() . A = F₄(A,(F₅() | A)) and
A5: dom F₆() = F₁() and
A6: ( 0 in F₁() implies F₆() . 0 = F₂() ) and
A7: for A being Ordinal st succ A in F₁() holds
F₆() . (succ A) = F₃(A,(F₆() . A)) and
A8: for A being Ordinal st A in F₁() & A <> 0 & A is limit_ordinal holds
F₆() . A = F₄(A,(F₆() | A))