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

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