scheme :: RECDEF_1:sch 10
LambdaSeqBinOpUn{ F1() -> FinSequence, F2( object , object ) -> object , F3() -> object , F4() -> object } :
F3() = F4()
provided
A1: ex p being FinSequence st
( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) and
A2: ex p being FinSequence st
( F4() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )