scheme :: ORDINAL2:sch 18
LambdaRecEx{ F₁() -> set , F₂( set , set ) -> set } :

ex f being Function st
( dom f = omega & f . 0 = F₁() & ( for n being Nat holds f . (succ n) = F₂(n,(f . n)) ) )