scheme :: RECDEF_2:sch 5
LambdaRec2ExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄( object , object , object ) -> Element of F₁() } :

ex f being sequence of F₁() st
( f . 0 = F₂() & f . 1 = F₃() & ( for n being Nat holds f . (n + 2) = F₄(n,(f . n),(f . (n + 1))) ) )