scheme :: ORDINAL1:sch 3
TSUniq{ F₁() -> Ordinal, F₂( Sequence) -> set , F₃() -> Sequence, F₄() -> Sequence } :

F₃() = F₄()

provided

A1: ( dom F₃() = F₁() & ( for B being Ordinal
for L being Sequence st B in F₁() & L = F₃() | B holds
F₃() . B = F₂(L) ) ) and
A2: ( dom F₄() = F₁() & ( for B being Ordinal
for L being Sequence st B in F₁() & L = F₄() | B holds
F₄() . B = F₂(L) ) )