scheme :: AFINSQ_1:sch 2
XSeqLambda{ F₁() -> Nat, F₂( object ) -> object } :

ex p being XFinSequence st
( len p = F₁() & ( for k being Nat st k in F₁() holds
p . k = F₂(k) ) )