scheme :: FINSEQ_4:sch 2
PiLambdaD{ F₁() -> non empty set , F₂() -> Nat, F₃( set ) -> Element of F₁() } :

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