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

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