scheme :: ORDINAL1:sch 4
TSExist{ F1() -> Ordinal, F2( Sequence) -> set } :
ex L being Sequence st
( dom L = F1() & ( for B being Ordinal
for L1 being Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1) ) )