scheme :: RECDEF_1:sch 5
SeqBinOpEx{ F₁() -> FinSequence, P₁[ object , object , object ] } :

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₁[F₁() . (k + 1),p . k,p . (k + 1)] ) )

provided

A1: for k being Nat
for x being set st 1 <= k & k < len F₁() holds
ex y being set st P₁[F₁() . (k + 1),x,y]