scheme :: RECDEF_1:sch 9
SeqBinOpUn{ F₁() -> FinSequence, P₁[ object , object , object ], F₂() -> object , F₃() -> object } :

F₂() = F₃()

provided

A1: for k being Nat
for x, y1, y2, z being set st 1 <= k & k < len F₁() & z = F₁() . (k + 1) & P₁[z,x,y1] & P₁[z,x,y2] holds
y1 = y2 and
A2: ex p being FinSequence st
( F₂() = 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)] ) ) and
A3: ex p being FinSequence st
( F₃() = 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)] ) )