scheme :: AFINSQ_2:sch 1
XSeqLambdaD{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

ex p being XFinSequence of F₂() st
( len p = F₁() & ( for j being Nat st j in F₁() holds
p . j = F₃(j) ) )