scheme :: FINSEQ_1:sch 2
SeqLambda{ F1() -> Nat, F2( object ) -> object } :
ex p being FinSequence st
( len p = F1() & ( for k being Nat st k in dom p holds
p . k = F2(k) ) )