scheme :: RECDEF_2:sch 4
LambdaRec2Ex{ F₁() -> set , F₂() -> set , F₃( object , object , object ) -> object } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & f . 1 = F₂() & ( for n being Nat holds f . (n + 2) = F₃(n,(f . n),(f . (n + 1))) ) )