scheme :: RECDEF_1:sch 6
LambdaSeqBinOpEx{ F₁() -> FinSequence, F₂( object , object ) -> set } :

ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) )