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

ex z being FinSequence of F₂() st
( len z = F₁() & ( for j being Nat st j in dom z holds
z . j = F₃(j) ) )