scheme :: RECDEF_1:sch 10
LambdaSeqBinOpUn{ F₁() -> FinSequence, F₂( object , object ) -> object , F₃() -> object , F₄() -> object } :

F₃() = F₄()

provided

A1: 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 . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) 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 . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) )