scheme :: ALGSEQ_1:sch 1
AlgSeqLambdaF{ F1() -> non empty ZeroStr , F2() -> Nat, F3( Nat) -> Element of F1() } :
ex p being AlgSequence of F1() st
( len p <= F2() & ( for k being Nat st k < F2() holds
p . k = F3(k) ) )