scheme :: RECDEF_2:sch 8
LambdaRec3Ex{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( object , object , object , object ) -> object } :

ex f being Function st
( dom f = NAT & 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))) ) )