scheme :: ORDINAL1:sch 4
TSExist{ F₁() -> Ordinal, F₂( Sequence) -> set } :

ex L being Sequence st
( dom L = F₁() & ( for B being Ordinal
for L1 being Sequence st B in F₁() & L1 = L | B holds
L . B = F₂(L1) ) )