scheme :: ALGSEQ_1:sch 1
AlgSeqLambdaF{ F₁() -> non empty ZeroStr , F₂() -> Nat, F₃( Nat) -> Element of F₁() } :

ex p being AlgSequence of F₁() st
( len p <= F₂() & ( for k being Nat st k < F₂() holds
p . k = F₃(k) ) )